[Haskell-cafe] Safe lists with GADT's

[Neil Mitchell]

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:

> 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)

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]

Any help or hints would be appreciated,

Thanks

Neil