[Haskell-cafe] Aren't type system extensions fun?
stansife at caltech.edu
Mon May 26 19:19:14 EDT 2008
> 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/
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
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
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)"?
More information about the Haskell-Cafe