On 10/24/07, <b class="gmail_sendername">Peter Hercek</b> <<a href="mailto:peter@syncad.com">peter@syncad.com</a>> wrote:<div><span class="gmail_quote"></span><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
I do not see why forall can be lifted to the top of function arrows.<br> I probably do not understand the notation at all. They all seem to be<br> different to me.</blockquote><div><br>Consider this simple function:<br>
<br> \b x y -> if b then x else y<br><br>Let's say we wanted to translate that into a language like System F, where every lambda has to have a type. We could write something like:<br><br> \(b::Bool) (x::?) (y::?) -> if b then x else y
<br><br>but we need something to put in those question marks. We solve this by taking the type of x and y as an additional parameter:<br><br> \(a::*) (b::Bool) (x::a) (y::a) -> if b then x else y<br><br>This would have the type "forall a. Bool -> a -> a -> a". In a dependently typed system, we might write that type as "(a::*) -> (b::Bool) -> (x::a) -> (y::a) -> a".
<br><br>Since b doesn't depend on a, we can switch their order in the argument list,<br><br> \(b::Bool) (a::*) (x::a) (y::a) -> if b then x else y<br><br>This has type "Bool -> forall a. a -> a -> a" or "(b::Bool) -> (a::*) -> (x::a) -> (y::a) -> a".
<br><br>Haskell arranges things so that the implicit type arguments always appear first in the argument list.<br><br>I find it helps to think of forall a. as being like a function, and exists a. as being like a pair.<br></div>
</div><br>-- <br>Dave Menendez <<a href="mailto:dave@zednenem.com">dave@zednenem.com</a>><br><<a href="http://www.eyrie.org/~zednenem/">http://www.eyrie.org/~zednenem/</a>>