Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Encoding "Less Than" with Haskell

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.

like image 427
Ranjit Jhala Avatar asked Jul 10 '13 18:07

Ranjit Jhala


1 Answers

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
like image 196
Toxaris Avatar answered Nov 14 '22 23:11

Toxaris