projects
/
lambda.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
4acb0dc
)
edits
author
Chris Barker
<barker@kappa.(none)>
Sun, 3 Oct 2010 01:06:52 +0000
(21:06 -0400)
committer
Chris Barker
<barker@kappa.(none)>
Sun, 3 Oct 2010 01:06:52 +0000
(21:06 -0400)
week4.mdwn
patch
|
blob
|
history
diff --git
a/week4.mdwn
b/week4.mdwn
index
9175c4a
..
ca6eb4c
100644
(file)
--- a/
week4.mdwn
+++ b/
week4.mdwn
@@
-288,8
+288,8
@@
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
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
+represented by the function `\x.x false 0`, one must have type (τ
+--> τ --> &tau) --> &sigma --> σ. 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
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