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

[Ryan Ingram]

On 5/28/08, Isaac Dupree <isaacdupree at charter.net> wrote:
> Andrew Coppin wrote:
> > 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!]
> >
>
> they're the same type: foralls in function *results* can be moved to the
> outside with no change in meaning.  They don't make it a higher rank type.
> (though some definitions in typically-uncurried languages like to call it
> higher rank, that's not relevant to us).  (modulo GHC issues with
> impredicative polymorphism, which ideally shouldn't even come into the
> picture here, because you're only using/exploring RankNTypes)

To be clear, these types are different but it doesn't matter because
we are also given a "type-abstraction" rule which allows us to convert
between the two trivially.

For example, given:

> const :: forall a b. a -> b -> a
> const2 :: forall a. a -> (forall b. b -> a)

When you partially apply const, you need to specify a type for the
second argument (see the previous person talking about "locking down"
type variables at the call site).

However, you don't know what type to lock down "b" to, so you can let
your caller choose!  Here's an example...

> test = const (1 :: Int)

What is the type of test?  First we need to "lock down" the types for
const; part of that involves generating a type variable for the "a"
and "b" arguments for const; while the "a" argument unifies with Int,
it turns out the "b" type variable is never used, so we allow the user
to choose it, ending up with the result:

> test :: forall b. b -> Int

The reason why you can always move a "forall" to the left of a
function arrow is very simple; given a type A (that may have some type
variables, but no "b"s.), and a type B (that may have some type
variables, including "b"), consider these two types:

type t1 = forall b. (A -> B)
type t2 = A -> (forall b. B)

To convert from t1 to t2, since A has no mention of the type variable
"b", we just delay the decision of what "b" should be.  In system F
notation, given an expression e1 of type t1, we can convert it to t2
in the following way:

] e2 :: t2
] e2 = \(a :: A) -> /\ b -> e1 @b a

Similarily, given an expression e2 of type t2, we can convert to t1:

] e1 :: t1
] e1 = /\ b -> \(a :: A) -> e2 a b

However, if we have a higher ranked type:

type t3 = (forall b. B) -> A
type t4 = forall b. (B -> A)

this conversion no longer works!  This is because expressions of type
t3 may call their arguments at many instances of b.  We can, however,
convert an expression e4 of type t4 into the higher-ranked type t3:

] e3 :: t3
] e3 = \(x :: forall b. B) -> e4 @Int (x @Int)

Notice that we had to choose some arbitrary type (I picked Int) to
instantiate x at when calling e4; this shows that the rank-2 type is
definitely different than the rank-1 type; it leaves more choices up
to the callee!

  -- ryan