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