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

[David Menendez]

On 10/24/07, Peter Hercek <peter at syncad.com> 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.


Consider this simple function:

    \b x y -> if b then x else y

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:

    \(b::Bool) (x::?) (y::?) -> if b then x else y

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:

    \(a::*) (b::Bool) (x::a) (y::a) -> if b then x else y

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".

Since b doesn't depend on a, we can switch their order in the argument list,

    \(b::Bool) (a::*) (x::a) (y::a) -> if b then x else y

This has type "Bool -> forall a. a -> a -> a" or "(b::Bool) -> (a::*) ->
(x::a) -> (y::a) -> a".

Haskell arranges things so that the implicit type arguments always appear
first in the argument list.

I find it helps to think of forall a. as being like a function, and exists
a. as being like a pair.

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20071024/f6b49f5a/attachment.htm