[Haskell-cafe] Safe lists with GADT's
Stefan O'Rear
stefanor at cox.net
Sun Feb 25 17:58:03 EST 2007
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
More information about the Haskell-Cafe
mailing list