[Haskell-cafe] Re: Aren't type system extensions fun? [Further insight]

[Lennart Augustsson]

These things become easier if you are explicit about type applications
(which Haskell isn't).
Phillippa mentioned it in an earlier post, but here it is again.

First the old stuff, if you have a term of type (S->T) then the
(normal form of) term must be (\ x -> e), where x has type S and e has
type T.
When using a function it's the caller that decided the actual value of
the x, and the callee decides the value to return.

OK, now forall.  If a term is of type (forall a . T) then the (normal
form of) term must be (/\ a -> e), where /\ is a capital lambda, and
it means it's a function that takes a type as the argument instead of
a term.  For type application I'll write f at T, meaning that f is /\
function and we give it type argument T.

Let's try it on some functions.  What's the real type id?  It's
id :: forall a . a-> a
since the type is a forall, the body of the function must start with a /\
id = /\ b -> \ x -> x
(or if you want to be explicit about types id= /\ b -> \ (x::b) -> x)
It's quite clear that the caller gets to pick both the type argument
and the value argument, and the id function only gets to pick the
return value,
e.g., (id at Int 5) or (id at Bool True).

Another example
const :: forall a . forall b . a -> b -> a
const = /\ a -> /\ b -> \ x -> \ y -> x
or, alternatively
const' :: forall a . a -> forall b . b -> a
const' = /\ a -> \ x -> /\ b -> \ y -> x
It's obvious that the caller gets to pick both types and both values.
The placement of the foralls only affect the type application order
(const at Int@Bool 5 True) resp (const'@Int 5 @Bool True).

All right, so let's do rank 2.
f :: (forall a . a -> a) -> (Int, Bool)
What's the body of the function?  The top level type is -> so it must
start with a \, e.g., \ g ->
When using g it must be used correctly.  The type of g starts with a
forall, so using it must start with a type application followed by a
normal application.
f = \ g -> (g at Int 5, g at Bool True)
So it's again clear the the caller of f doesn't get to pick the type
a, it must be supplied by the callee.  The caller of f must supply a
value of type (forall a . a->a), i.e., (f id).

So you can see that depending on the forall's position with respect to
the -> the role of it changes from a type being picked by the caller
or callee.
(If it's under an odd number of arrows the callee picks.)

If you remove all the explicit type abstractions and applications
above then you have Haskell (+ RankN).
As other have pointed out, you can't remove the nested foralls because
in general they cannot be inferred.

Hope this helps.

  -- Lennart



On Wed, May 28, 2008 at 7:51 PM, Andrew Coppin
<andrewcoppin at btinternet.com> wrote:
> Luke Palmer wrote:
>>
>> When you're reasoning about this, I think it would help you greatly to
>> explicitly put in *all* the foralls.  In haskell, when you write, say:
>>
>>   map :: (a -> b) -> [a] -> [b]
>>
>> All the free variables are *implicitly* quantified at the top level.
>> That is, when you write the above, the compiler sees:
>>
>>   map :: forall a b. (a -> b) -> [a] -> [b]
>>
>> And the type you mention above for the strange expression is:
>>
>>   forall x. (x -> x) -> (Char, Bool)
>>
>> Which indicates that the caller gets to choose.  That is, if a caller
>> sees a 'forall' at the top level, it is allowed to instantiate it with
>> whatever type it likes.   Whereas the type you want has the forall in
>> a different place than the implicit quantifiaction:
>>
>>   (forall x. x -> x) -> (Char, Bool)
>>
>> Here the caller does not have a forall at the top level, it is hidden
>> inside a function type so the caller cannot instantiate the type.
>> However, when implementing this function, the argument will now have
>> type
>>
>>    forall x. x -> x
>>
>> And the implementation can instantiate x to be whatever type it likes.
>>
>
> Hmm. Right. So you're saying that the exact position of the "forall"
> indicates the exact time when the variable(s) get specific types assigned to
> them?
>
> So... the deeper you nest the foralls, the longer those variables stay
> unbound? [And the higher the "rank" of the type?]
>
> Finally, that seems to make actual sense. I have one final question though:
>
>  forall x, y. x -> y -> Z
>  forall x. x -> (forall y. y -> Z)
>
> Are these two types the same or different? [Ignoring for a moment the
> obvious fact that you'll have one hell of a job writing a total function
> with such a type!] After all, ignoring the quantification, we have
>
>  x -> y -> Z
>  x -> (y -> Z)
>
> which are both the same type. So does that mean you can move the forall to
> the left but not to the right? Or are the types actually different?
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>