[Haskell-cafe] Safe lists with GADT's

[Derek Elkins]

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