System F|http://www.cis.upenn.edu/~bcpierce/tapl/index.html]] (the
relevant evaluator is called "fullpoly"):
- N = All X . (X->X)->X->X;
+ N = ∀ α . (α->α)->α->α;
Pair = (N -> N -> N) -> N;
- let zero = lambda X . lambda s:X->X . lambda z:X. z in
+ let zero = lambda α . lambda s:α->α . lambda z:α. z in
let fst = lambda x:N . lambda y:N . x in
let snd = lambda x:N . lambda y:N . y in
let pair = lambda x:N . lambda y:N . lambda z:N->N->N . z x y in
- let suc = lambda n:N . lambda X . lambda s:X->X . lambda z:X . s (n [X] s z) in
+ let suc = lambda n:N . lambda α . lambda s:α->α . lambda z:α . s (n [α] s z) in
let shift = lambda p:Pair . pair (suc (p fst)) (p fst) in
let pre = lambda n:N . n [Pair] shift (pair zero zero) snd in
The key to the extra expressive power provided by System F is evident
in the typing imposed by the definition of `pre`. The variable `n` is
-typed as a Church number, i.e., as `All X . (X->X)->X->X`. The type
+typed as a Church number, i.e., as `∀ α . (α->α)->α->α`. The type
application `n [Pair]` instantiates `n` in a way that allows it to
manipulate ordered pairs: `n [Pair]: (Pair->Pair)->Pair->Pair`. In
other words, the instantiation turns a Church number into a
to replace the type for Church numbers with a concrete (simple) type,
we would have to replace each `X` with the type for Pairs, `(N -> N ->
N) -> N`. But then we'd have to replace each of these `N`'s with the
-type for Church numbers, `(X -> X) -> X -> X`. And then we'd have to
-replace each of these `X`'s with... ad infinitum. If we had to choose
+type for Church numbers, `(α -> α) -> α -> α`. And then we'd have to
+replace each of these `α`'s with... ad infinitum. If we had to choose
a concrete type built entirely from explicit base types, we'd be
unable to proceed.
In fact, unlike in the simply-typed lambda calculus,
it is even possible to give a type for ω in System F.
-<code>ω = lambda x:(All X. X->X) . x [All X . X->X] x</code>
+<code>ω = lambda x:(∀ α. α->α) . x [∀ α . α->α] x</code>
In order to see how this works, we'll apply ω to the identity
function.
<code>ω id ==</code>
- (lambda x:(All X . X->X) . x [All X . X->X] x) (lambda X . lambda x:X . x)
+ (lambda x:(∀ α . α->α) . x [∀ α . α->α] x) (lambda α . lambda x:α . x)
-Since the type of the identity function is `(All X . X->X)`, it's the
+Since the type of the identity function is `(∀ α . α->α)`, it's the
right type to serve as the argument to ω. The definition of
ω instantiates the identity function by binding the type
-variable `X` to the universal type `All X . X->X`. Instantiating the
+variable `α` to the universal type `∀ α . α->α`. Instantiating the
identity function in this way results in an identity function whose
type is (in some sense, only accidentally) the same as the original
fully polymorphic identity function.
With these basic types, we want to say something like this:
and:t->t->t = lambda l:t . lambda r:t . l r false
- and = lambda 'a . lambda 'b .
- lambda l:'a->'b . lambda r:'a->'b .
- lambda x:'a . and:'b (l x) (r x)
+ and = lambda α . lambda β .
+ lambda l:α->β . lambda r:α->β .
+ lambda x:α . and:β (l x) (r x)
The idea is that the basic *and* conjoins expressions of type `t`, and
when *and* conjoins functional types, it builds a function that
of *and* in the definition by using the result type. But fully
instantiating the definition as given requires type application to a
pair of types, not to just a single type. We want to somehow
-guarantee that 'b will always itself be a complex type.
+guarantee that β will always itself be a complex type.
So conjunction and disjunction provide a compelling motivation for
polymorphism in natural language, but we don't yet have the ability to