Encoding "Less Than" with Haskell

Question

am hoping some Haskell experts can help clarify something.

Is it possible to define Nat in the usual way (via @dorchard Singleton types in Haskell)

data S n = Succ n 
data Z   = Zero

class Nat n 
instance Nat Z
instance Nat n => Nat (S n)

(or some variant thereof) and then define a LessThan relation such that forall n and m

LessThan Z (S Z)
LessThan n m => LessThan n     (S m)
LessThan n m => LessThan (S n) (S m)

and then write a function with a type like:

foo :: exists n. (LessThan n m) => Nat m -> Nat n
foo (S n) = n
foo Z     = foo Z

I explicitly want to use the "LessThan" in the output type for foo, I realize that one could certainly write something like

foo :: Nat (S n) -> Nat n

but thats not what I'm after.

Thanks!

Ranjit.

Answer 1

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