From 8a2e3fac5b5faf8eebef6b4c24db35dfc101c07c Mon Sep 17 00:00:00 2001 From: Chris Date: Tue, 24 Feb 2015 16:43:38 -0500 Subject: [PATCH] edits --- topics/_week5_system_F.mdwn | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn index 2d9035a7..d7a2cf12 100644 --- a/topics/_week5_system_F.mdwn +++ b/topics/_week5_system_F.mdwn @@ -77,10 +77,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] @@ -142,13 +143,16 @@ 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. +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, chapter 23.] -- 2.11.0