From 9acc38db110615e798d115ccc71972713cee08d6 Mon Sep 17 00:00:00 2001 From: Chris Date: Tue, 24 Feb 2015 16:24:47 -0500 Subject: [PATCH] edits --- topics/_week5_system_F.mdwn | 51 ++++++++++++++++++++++++++++----------------- 1 file changed, 32 insertions(+), 19 deletions(-) diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn index f6f7ab6b..2d9035a7 100644 --- a/topics/_week5_system_F.mdwn +++ b/topics/_week5_system_F.mdwn @@ -115,13 +115,14 @@ System F|http://www.cis.upenn.edu/~bcpierce/tapl/index.html]] (the relevant evaluator is called "fullpoly"): N = All X . (X->X)->X->X; - Pair = All X . (N -> N -> X) -> X; + Pair = (N -> N -> N) -> N; let zero = lambda X . lambda s:X->X . lambda z:X. 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 X . lambda z:N->N->X . z x 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 shift = lambda p:Pair . p [Pair] (lambda a:N . lambda b:N . pair (suc a) a) in - let pre = lambda n:N . n [Pair] shift (pair zero zero) [N] snd 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 pre (suc (suc (suc zero))); @@ -132,27 +133,38 @@ lambda, though the difference is encoded in whether the variables are lower case (for ordinary lambda) or upper case (for type-level lambda). -The key to the extra flexibility provided by System F is that we can -instantiate the `pair` function to return a number, as in the -definition of `pre`, or we can instantiate it to return an ordered -pair, as in the definition of the `shift` function. Because we don't -have to choose a single type for all uses of the pair-building -function, we aren't forced into a infinite regress of types. - +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 +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 +pair-manipulating function, which is the heart of the strategy for +this version of predecessor. + +But of course, the type `Pair` (in this simplified example) is defined +in terms of Church numbers. If we tried to replace the type for +Church numbers with a concrete (simple) type, we would have to replace +each `X` with `(N -> N -> N) -> N`. But then we'd have to replace +each `N` with `(X -> X) -> X -> X`. And then replace each `X` +with... ad infinitum. If we had to choose a concrete type built +entirely from explicit base types, we'd be unable to proceed. + [See Benjamin C. Pierce. 2002. *Types and Programming Languages*, MIT -Press, pp. 350--353, for `tail` for lists in System F.] +Press, chapter 23.] Typing ω -------------- -In fact, it is even possible to give a type for ω in System F. +In fact, unlike in the simply-typed lambda calculus, +it is even possible to give a type for ω in System F. ω = lambda x:(All X. X->X) . x [All X . X->X] x In order to see how this works, we'll apply ω to the identity function. -ω [All X . X -> X] id == +ω id == (lambda x:(All X . X->X) . x [All X . X->X] x) (lambda X . lambda x:X . x) @@ -161,11 +173,11 @@ 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 identity function in this way results in an identity function whose -type is the same as the original fully polymorphic identity function. +type is (in some sense, only accidentally) the same as the original +fully polymorphic identity function. So in System F, unlike in the simply-typed lambda calculus, it *is* -possible for a function (in this case, the identity function) to apply -to itself! +possible for a function to apply to itself! Does this mean that we can implement recursion in System F? Not at all. In fact, despite its differences with the simply-typed lambda @@ -177,8 +189,9 @@ form in a finite number of steps. Not only does a fixed-point combinator remain out of reach, we can't even construct an infinite loop. This means that although we found a type for ω, there is no general type for Ω ≡ ω -ω. (It turns out that no Turing complete system can be strongly -normalizing, from which it follows that System F is not Turing complete.) +ω. Furthermore, it turns out that no Turing complete system can +be strongly normalizing, from which it follows that System F is not +Turing complete. Types in OCaml -- 2.11.0