[Haskell-cafe] Re: Safe lists with GADT's
apfelmus at quantentunnel.de
apfelmus at quantentunnel.de
Mon Feb 26 05:15:35 EST 2007
Stefan O'Rear wrote:
>> 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:
Indeed, you can't. I mean, given
fromList [] = Nil
fromList (a:as) = Cons a (fromList as)
what type would it have? One of
fromList :: forall t . [a] -> List a t
fromList :: [a] -> List a NilT
fromList :: forall t . [a] -> List a (ConsT t)
? No, because the second argument depends on the input list. The only
thing we know is that there is a type t but we don't know which one. Thus
fromList :: [a] -> (exists t . List a t)
is the correct type. As Haskell currently doesn't have "first class
existentials", we have to either pack it into a data type or appeal to
the equivalence
exists a . f a ~= forall r . (forall a . f a -> r) -> r
Both have of course the problem that we cannot simply write
safeMap (fromList [1,2,3]) :: exists t . List a t
Regards,
apfelmus
Exercise: Why is
fromList :: exists t . [a] -> List a t
wrong as well?
More information about the Haskell-Cafe
mailing list