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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
