[Haskell-cafe] Aren't type system extensions fun?

[Eric Stansifer]

> Well anyway, I was under the impression that id :: x -> x, so I'm not really
> sure why this wouldn't work without Rank-2 types...

The matter at hand is the type of the function /f/, not of the
function /id/.  I'll address the question of applying /f/ to /id/ at
the end, but the interesting question is how to assign a type to /f/
at all.

In Bob's example,
f g x = (g g) x
let us try to give /f/ a type.

The rank-1 type we might first attempt is:
f :: (a -> a) -> a -> a
(which is the same thing as /f :: forall a. (a -> a) -> a -> a/).  But
under this type, we would have /g :: a -> a/, and then the expression
/g g/ is illegal.

If we try again,
f :: ((a -> a) -> (a -> a)) -> a -> a
we again find that the expression /g g/ is illegal.  Experimenting
further along this line will quickly convince you of the difficulty of
typing /f/.

However, it can be done using rank-2 types:

> f :: (forall a. a -> a) -> b -> b
> f g x = (g g) x

In the expression /g g/, both /g/s have the same rank-1 type /forall
a. a -> a/ (which is the same as the type /a -> a/);  in the second
usage of /g/, we assign /b/ to the type variable /a/, and in the first
usage of /g/, we assign /b -> b/ to the type variable /a/.  (Thus, the
second usage of /g/ has type /a -> a/, and the first usage has type
/(a -> a) -> (a -> a)/.)  This is the essential point of the /forall
a/ -- it allows the type variable /a/ to be instantiated differently
as /g/ is used in different places.  In other words, it is
polymorphic.

Going back to /id/, recall that
id :: a -> a
which is the same thing as
id :: forall a. a -> a
(i.e., /id/ is a polymorphic function).  Since the type of /id/
unifies with the first argument of /f/, the function application /f
id/ is well-typed.


Note that we could "simplify" Bob's example down to:
f2 g = g g
although the type of this /f2/ is less pleasant:
f2 :: (forall a. a -> a) -> (forall a. a -> a)

Say, wouldn't a syntax like "(forall a => a -> a)" or "(a => a -> a)"
or something similar to that be more consistent with syntax for
contexts, e.g. "(Ord a => a -> a)"?

Eric