From oleg-at-okmij.org Sat Aug 14 04:10:04 2004
To: haskell@haskell.org
Subject: Re: Dependent Types in Haskell
In-Reply-To: <16665.37498.850242.394772@sf0.comp.nus.edu.sg>
From: oleg-at-pobox.com
Message-ID: <20040814101004.D7741AB7E@Adric.metnet.navy.mil>
Date: Sat, 14 Aug 2004 03:10:04 -0700 (PDT)
Status: OR
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 specify 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
The sum-of-lengths property, although it is not derived by the
typechecker as the consequence of the `appnd' definition, nevertheless
must be consistent with that definition. If we state the property
wrongly, the error will be caught by the typechecker when we _use_
|vapp| with the argument lists that expose the error.
> testl3 = vapp testl1 testl2
The inferred type of testl3 is
*LL> :t testl3
testl3 :: Cons (Cons (Cons (Cons (Cons (Nil Z) (S Z)) (S (S Z)))
(S (S (S Z))))
(S (S (S (S Z)))))
(S (S (S (S (S Z)))))
Int
and its value is
*LL> testl3
Cons 3 (Cons 2 (Cons 1 (Cons 2 (Cons 1 Nil))))