[Haskell-cafe] Safe lists with GADT's

[Neil Mitchell]

Hi Stefan,

> 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:
>

> -- 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))

How do I get my original function back which just turns a standard
list to one of the funky lists, or is that just impossible with
GADT's? Do I now have to "wrap" all the fuctions I use, i.e. pass
safeMap in CPS?

Thanks

Neil