From 014db35e12f61a3192007298c2db56b5843f79d1 Mon Sep 17 00:00:00 2001 From: Chris Barker Date: Sat, 2 Oct 2010 21:08:05 -0400 Subject: [PATCH] edits --- week4.mdwn | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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. -- 2.11.0