X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=15349c4cffee0c16ff565284fc13870c6ee07d7e;hp=7cd8a921dbfebc07558180aa7717a3b83e0cd0d5;hb=2ba6b449af8d0d819018bbf7c00b1ec40625b5ab;hpb=5dad3bae051905473c6cc3d01bf261cbcce0968e diff --git a/week4.mdwn b/week4.mdwn index 7cd8a921..15349c4c 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -287,15 +287,15 @@ functions, one for each type. Version 1 type numerals are not a good choice for the simply-typed lambda calculus. The reason is that each different numberal has a different type! For instance, if zero has type σ, then `false` -has type τ --> τ --> &tau, for some τ. Since one is -represented by the function `\x.x false 0`, one must have type `(τ ---> τ --> &tau) --> &sigma --> σ`. But this is a different +has type τ --> τ --> τ, for some τ. Since one is +represented by the function `\x.x false 0`, one must have type (τ +--> τ --> τ) --> σ --> σ. But this is a different type than zero! Because each number has a different type, it becomes impossible to write arithmetic operations that can combine zero with one. We would need as many different addition operations as we had pairs of numbers that we wanted to add. Fortunately, the Church numberals are well behaved with respect to -types. They can all be given the type `(σ --> σ) --> -σ --> σ`. +types. They can all be given the type (σ --> σ) --> +σ --> σ.