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.

foo :: exists n... – really? So you want to allow foo to return any type it likes, with the only constraint that it be "less than m"? That's not possible in Haskell (not just like that), and rightly so. Or do you rather mean, foo can return any type the caller requests, as long as it's less than m? — leftaroundabout
"some" seems interchangable with "any" in that sentence. The crucial question is: who decides which type it's going to be? — leftaroundabout
No one decides, I just want a spec that says "the output is some nat that is strictly less than the input" (without saying what that number is...) — Ranjit Jhala
So deciding the type is up to the function (or the guy how implements it, if you prefer that)? — leftaroundabout
@MonadNewb This is type level programming, which is used for some ultra-cunning type tricks. Ranjit is encoding the integers in the type system as opposed to as data, which is why LessThan needs to be in the type system too. It's safe to ignore type level programming until you're very confident with Haskell. — AndrewC

Toxaris Toxaris · Accepted Answer · 2013-07-11T01:00:51

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