From: Chris Barker Date: Sun, 3 Oct 2010 01:08:05 +0000 (-0400) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=014db35e12f61a3192007298c2db56b5843f79d1 edits --- diff --git a/week4.mdwn b/week4.mdwn index 15349c4c..d46981e0 100644 --- 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 -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.