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:
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)
You need to use existentials. The following code hides one in its definition: fromList :: [a] -> (List a NilT -> r) -> (forall b. List a (ConsT b) -> r) -> r fromList [] nilk consk = nilk Nil fromList (x:xs) nilk consk = fromList' xs (consk . Cons x) where fromList' :: [a] -> (forall b. List a b -> r) -> r fromList' [] k = k Nil fromList' (x:xs) k = fromList' xs (k . Cons x) Also it should be possible to arrange this to use a very simple library for existentials I made, made possible by GHC 6.6's new support for impredicativity. -- exists a. F a -- <=> exists a.not (not (F a)) -- <=> not (forall a.not (F a)) type Exists f = forall r.(forall a.(f a -> r)) -> r open :: Exists f -> (forall a.(f a -> r)) -> r open package k = package k pack :: f a -> Exists f pack a k = k a