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?