[Haskell-cafe] Safe lists with GADT's

Stefan O'Rear stefanor at cox.net
Sun Feb 25 18:22:21 EST 2007


On Sun, Feb 25, 2007 at 11:11:14PM +0000, Neil Mitchell wrote:
> 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?

AFAIK you can't. Fortunately the CPS transform can be very local:

-- write this as you normally would, no cps at all
do_something_with_safe_list :: List t a -> (something -> somethingelse ...) --assoc for clarity

do_something_with_unsafe_list :: [a] -> (same as above)
do_something_with_unsafe_list ls = fromListC ls do_something_with_safe_list


More information about the Haskell-Cafe mailing list