X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week5_system_F.mdwn;h=b8c6bf3da6d93c05a1e16ea6ef7ec94528ea3f60;hp=f6f7ab6b264015d6a7ae57040acba64b4411a2d1;hb=ecea9a7ecaae77c1da240a683caca592b909e32c;hpb=38831ff5ac8222c8d44dce54d3c52c7fa09af3bf diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn index f6f7ab6b..b8c6bf3d 100644 --- a/topics/_week5_system_F.mdwn +++ b/topics/_week5_system_F.mdwn @@ -1,3 +1,5 @@ +[[!toc]] + # System F and recursive types In the simply-typed lambda calculus, we write types like σ @@ -77,10 +79,11 @@ tick marks, Grecification, or capitalization), there is no need to distinguish expression abstraction from type abstraction by also changing the shape of the lambda. -This expression is a polymorphic version of the identity function. It -defines one general identity function that can be adapted for use with -expressions of any type. In order to get it ready to apply this -identity function to, say, a variable of type boolean, just do this: +The expression immediately below is a polymorphic version of the +identity function. It defines one general identity function that can +be adapted for use with expressions of any type. In order to get it +ready to apply this identity function to, say, a variable of type +boolean, just do this: (Λ 'a (λ x:'a . x)) [t] @@ -115,13 +118,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 +136,41 @@ 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. + +Could we try to build a system for doing Church arithmetic in which +the type for numbers always manipulated ordered pairs? The problem is +that the ordered pairs we need here are pairs of numbers. If we tried +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 +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 +179,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 +195,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