[Haskell-cafe] Safe lists with GADT's

[Stefan O'Rear]

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