projects
/
lambda.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
2ba6b44
)
edits
author
Chris Barker
<barker@kappa.(none)>
Sun, 3 Oct 2010 01:08:05 +0000
(21:08 -0400)
committer
Chris Barker
<barker@kappa.(none)>
Sun, 3 Oct 2010 01:08:05 +0000
(21:08 -0400)
week4.mdwn
patch
|
blob
|
history
diff --git
a/week4.mdwn
b/week4.mdwn
index
15349c4
..
d46981e
100644
(file)
--- a/
week4.mdwn
+++ b/
week4.mdwn
@@
-270,9
+270,9
@@
cannot have a type in Λ_T. We can easily see why:
Assume Ω has type τ, and `\x.xx` has type σ. Then
because `\x.xx` takes an argument of type σ and returns
Assume Ω has type τ, and `\x.xx` has type σ. Then
because `\x.xx` takes an argument of type σ and returns
-something of type τ, `\x.xx` must also have type
`
σ -->
-τ
`
. By repeating this reasoning, `\x.xx` must also have type
-
`(σ --> τ) --> τ`
; and so on. Since variables have
+something of type τ, `\x.xx` must also have type σ -->
+τ. By repeating this reasoning, `\x.xx` must also have type
+
(σ --> τ) --> τ
; and so on. Since variables have
finite types, there is no way to choose a type for the variable `x`
that can satisfy all of the requirements imposed on it.
finite types, there is no way to choose a type for the variable `x`
that can satisfy all of the requirements imposed on it.