[Haskell-cafe] Re: Existential types (Was: Type vs TypeClass duality)

[apfelmus]

Peter Hercek wrote:
> I do not see why forall can be lifted to the top of function arrows.
>  I probably do not understand the notation at all. They all seem to be
>  different to me.
> 
>  String -> ∀a.a
> a function which takes strings a returns a value of all types together
>  for any input string (so only bottom could be the return value?)
> 
>  ∀a.(String -> a)
> a function which takes strings and returns a values of a type we want
>  to be returned (whichever one it is; in given  contexts the return
>  value type is the same for all input strings)

It's probably best to interpret ∀a as "you are to choose any type  a 
and I will comply". Then, it doesn't matter whether you first supply a 
String and then choose some  a  or whether you first choose some  a  and 
then supply a String. In both cases, the choice is yours and independent 
of the String. So, the types

   String -> ∀a.a  and  ∀a.(String -> a)

are isomorphic. (And you're right, the only thing this function can do 
is to return _|_.)

In contrast, ∃a means "I choose a concrete type  a  at will and you will 
have to deal with all of my capricious choices".

Regards,
apfelmus