[Haskell] Re: Dependent Types in Haskell

[oleg at pobox.com]

Martin Sulzmann stated the goal of the append exercise as follows:

] Each list carries now some information about its length.
] The type annotation states that the sum of the output list
] is the sum of the two input lists.

I'd like to give a Haskell implementation of such an append
function, which makes an extensive use of partial signatures and, in
generally, relies on the compiler to figure out the rest of the
constraints. We also separate the skeleton of the list from the type
of the list elements.

This solution differs from the Haskell solution append3.hs given in
Martin Sulzmann's message. The latter solution relies on the trusted
kernel: the equality datatype E. It is quite easy to subvert
append3.hs if we set up E with particular run-time values. The error
will not be discovered statically -- nor dynamically for that matter,
in the given code. We can get the function app to produce a non-bottom
list value whose dynamic size differs from its size type (and whose
static size is patently not the arithmetic sum of the static sizes of
the arguments).

The solution in this message relies entirely on Haskell type system;
there are no trusted terms. An attempt to write a terminating term
that is to produce a list whose length differs from that stated in the
term's type will be caught by the type checker at compile time.

> {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
>
> module LL where
>
> data Z; data S a

First we state the Sum constraint:

> class Add n m p | n m -> p
> instance Add Z a a
> instance Add n (S m) p => Add (S n) m p

Now we derive a number-parameterized list. We separate the shape
type of the list from the type of the list elements:

> data Nil  len a = Nil deriving Show
> data Cons b len a = Cons a (b a) deriving Show

The constraint `List f' holds iff f is the shape type of a valid list:

> class List ( lst :: * -> * )
> instance List (Nil Z)
> instance (Add (S Z) n m, List (tail n)) => List (Cons (tail n) m)

The following `type function' makes sure that its argument is a valid
list. That guarantee is established statically. We should note
that the class List has no members. Therefore, the only terminating term
with the signature `(List f) => f a -> f a' is the identity.

> make_sure_it_is_a_list:: (List f) => f a -> f a
> make_sure_it_is_a_list = id

> nil:: Nil Z a
> nil = Nil

We let the compiler write out the constraints for us:

> consSig :: a -> f l a -> Cons (f l) (S l) a
> consSig = undefined
> cons h t | False = consSig h t
> cons h t = make_sure_it_is_a_list$ Cons h t

We can create a few lists:

> testl1 = cons (3::Int) ( cons (2::Int) ( cons (1::Int) nil ) )
> testl2 =               ( cons (2::Int) ( cons (1::Int) nil ) )

The type of testl2 is reasonable:

	testl2 :: Cons (Cons (Nil Z) (S Z)) (S (S Z)) Int

If we try to cheat and write
     consSig :: a -> f l a -> Cons (f l) (S (S l)) a
the typechecker will point out that 'Z' is not equal to 'S Z' when
typechecking testl1 and testl2.

We can now handle Append:

> class Append l1 l2 l3 | l1 l2 -> l3 where
>     appnd :: l1 a -> l2 a -> l3 a
>
> instance Append (Nil Z) l l where
>     appnd _ l = l
>
> instance (Append (t n) l (t' n'), List (t' n'))
>     => Append (Cons (t n) (S n)) l (Cons (t' n') (S n')) where
>     appnd (Cons h t) l = cons h (appnd t l)
 
We had to be explicit with types in the latter instance. The types
must correspond to the term; the typechecker will tell us if they do
not.

We now attempt to verify the sum of lengths property. We attach the
desired constraints using the partial signature trick. This saves us
trouble enumerating all other constraints.

> constraintAdd:: Add l1 l2 l3 => (f1 l1 a) -> (f2 l2 a) -> (f3 l3 a)
> constraintAdd = undefined

> vapp l1 l2 | False = constraintAdd l1 l2
> vapp l1 l2 = appnd l1 l2

Perhaps we should move to Cafe?