From: Chris Date: Sun, 22 Feb 2015 14:03:42 +0000 (-0500) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=5e9e42542f2f56e0236af240519eda4cdde09a52 edits --- diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn index c3b1cf88..cee3f916 100644 --- a/topics/_week5_simply_typed_lambda.mdwn +++ b/topics/_week5_simply_typed_lambda.mdwn @@ -166,8 +166,31 @@ functions; but a simply-types identity function can never apply to itself. #Typing numerals# -The Church numerals are well behaved with respect to types. They can -all be given the type (σ --> σ) --> σ --> σ. +The Church numerals are well behaved with respect to types. +To see this, consider the first three Church numerals (starting with zero): + + \s z . z + \s z . s z + \s z . s (s z) + +Given the internal structure of the term we are using to represent +zero, its type must have the form ρ --> σ --> $sigma; for +some ρ and σ. This type is consistent with term for one, +but the structure of the definition of one is more restrictive: +because the first argument `s` must apply to the second argument `z`, +the type of the first argument must describe a function from +expressions of type σ to some other type. So we can refine ρ +by replacing it with the more specific type σ --> τ. At +this point, the overall type is (σ --> τ) --> σ --> +σ. Note that this refined type remains compatible with the +definition of zero. Finally, by examinine the definition of two, we +see that expressions of type τ must be suitable to serve as +arguments to functions of type σ --> τ. The most general +way for that to be true is if τ ≡ σ. So at this +point, we have the overall type of (σ --> σ) --> σ --> +σ. + + ## Predecessor and lists are not representable in simply typed lambda-calculus ##