Here's one way to implement something similar to what you ask about.
Nat
First note that you define Nat
as a class and then use it as a type. I think it makes sense to have it as a type, so let's define it as such.
data Z
data S n
data Nat n where
Zero :: Nat Z
Succ :: Nat n -> Nat (S n)
LessThan
We can also define LessThan
as a type.
data LessThan n m where
LT1 :: LessThan Z (S Z)
LT2 :: LessThan n m -> LessThan n (S m)
LT3 :: LessThan n m -> LessThan (S n) (S m)
Note that I just toke your three properties and turned them into data constructors. The idea of this type is that a fully normalized value of type LessThan n m
is a proof that n
is less than m
.
Work-around for existentials
Now you ask about:
foo :: exists n. (LessThan n m) => Nat m -> Nat n
But there exists no exists in Haskell. Instead, we can define a datatype just for foo
:
data Foo m where
Foo :: Nat n -> LessThan n m -> Foo m
Note that n
is effectively existenially quantified here, because it shows up in the arguments of the data constructor Foo
but not in its result. Now we can state the type of foo
:
foo :: Nat m -> Foo m
A lemma
Before we can implement the example from the question, we have to prove a little lemma about LessThan
. The lemma says that n
is less than S n
for all n
. We prove it by induction on n
.
lemma :: Nat n -> LessThan n (S n)
lemma Zero = LT1
lemma (Succ n) = LT3 (lemma n)
Implementation of foo
Now we can write the code from the question:
foo :: Nat m -> Foo m
foo (Succ n) = Foo n (lemma n)
foo Zero = foo Zero