On Sun, Feb 25, 2007 at 10:40:13PM +0000, Neil Mitchell wrote:
Hi
I'm starting to play with GADT's, and I was trying to write a safe version of head and tail, on a safe version of lists. What I came up with is:
[code moved later]
Defining safeMap was trivial, but one thing I couldn't figure out was how to write something like fromList:
fromList [] = Nil fromList (a:as) = Cons a (fromList as)
fromList could obviously be anything such as reading from a file etc, where the input is not known in advance. Are there any techniques for this?
In addition I was expecting to find some example like this in one of the papers/examples on GADT's, but I didn't. The Haskell wikibook has a slight example along these lines, but not with the recursive field in ConsT. [http://en.wikibooks.org/wiki/Haskell/GADT]
Since we don't know in advance the length of the list, we need an existensial type; this immediately causes problems because existential types do not exist in any current Haskell implementation. There are two approaches: \begin{code} data ConsT a data NilT data List a t where Cons :: a -> List a b -> List a (ConsT b) Nil :: List a NilT instance Show a => Show (List a t) where show (Cons a b) = show a ++ ":" ++ show b show Nil = "[]" safeHead :: List a (ConsT t) -> a safeHead (Cons a b) = a safeTail :: List a (ConsT t) -> List a t safeTail (Cons a b) = b safeMap :: (a -> b) -> List a t -> List b t safeMap f Nil = Nil safeMap f (Cons a b) = Cons (f a) (safeMap f b) -- Using an existential datatype box data VarList a = forall t. VarList (List a t) fromListV :: [a] -> VarList a fromListV [] = VarList Nil fromListV (x:xs) = case fromListV xs of VarList xs' -> VarList (Cons x xs') -- using CPS transform (turns existentials into rank2) -- generally prefered because it avoids naming a one-use data type, -- but YMMV fromListC :: [a] -> (forall t. List a t -> r) -> r fromListC [] fn = fn Nil fromListC (x:xs) fn = fromListC xs (\sl -> fn (Cons x sl)) \end{code} HTH Stefan