N = ∀α. (α->α)->α->α;
Pair = (N->N->N) -> N;
- let zero = α . λs:α->α . λz:α. z in
- let fst = λx:N . λy:N . x in
- let snd = λx:N . λy:N . y in
- let pair = λx:N . λy:N . λz:N->N->N . z x y in
- let suc = λn:N . λα . λlambda s:α->α . λz:α . s (n [α] s z) in
- let shift = λp:Pair . pair (suc (p fst)) (p fst) in
- let pre = λn:N . n [Pair] shift (pair zero zero) snd in
+ let zero = Î\9bα. λs:α->α . λz:α. z in
+ let fst = λx:N. λy:N . x in
+ let snd = λx:N. λy:N . y in
+ let pair = λx:N. λy:N . λz:N->N->N . z x y in
+ let suc = λn:N. λα . λlambda s:α->α . λz:α. s (n [α] s z) in
+ let shift = λp:Pair. pair (suc (p fst)) (p fst) in
+ let pre = λn:N. n [Pair] shift (pair zero zero) snd in
pre (suc (suc (suc zero)));
In fact, unlike in the simply-typed lambda calculus,
it is even possible to give a type for ω in System F.
-<code>ω = lambda 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:(∀ α . α->α) . x [∀ α . α->α] x) (lambda α . lambda x:α . x)
+ (λx:(∀α. α->α) . x [∀α.α->α] x) (Λα.λx:α. x)
-Since the type of the identity function is `(∀ α . α->α)`, 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 `α` to the universal type `∀ α . α->α`. 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 α . lambda β .
- lambda l:α->β . lambda r:α->β .
- lambda x:α . and:β (l x) (r x)
+ and:t->t->t = λl:t. λr:t. l r false
+ and = Λα.Λβ.λl:α->β.λr:α->β.λ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