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