[Haskell-cafe] Re: Safe lists with GADT's

[apfelmus at quantentunnel.de]

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?