X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=cps.mdwn;h=a3f0459515172dda78972e342b03cf9805f2ff88;hp=f869b7956f4f86e6a95309301c07d3fff8207075;hb=d12897af7d3a9b1946a084b0680a2bbb1fb1e57a;hpb=54360af5dafc49cca9e484ecdc74c26c4adfb65c

diff --git a/cps.mdwn b/cps.mdwn
index f869b795..a3f04595 100644
--- a/cps.mdwn
+++ b/cps.mdwn
@@ -216,9 +216,9 @@ for functional types a->b, (a->b)' = ((a' -> σ) -> σ) -> (b' -> &sig
 
     Terms                            Types
 
-    [x] = \k.xk                      [a] = (a'->σ)->σ
-    [\xM] = \k.k(\x[M])              [a->b] = ((a->b)'->σ)->σ
-    [MN] = \k.[M](\m.m[N]k)          [b] = (b'->σ)->σ
+    [x] = \k.xk                      [a] = (a'->o)->o
+    [\xM] = \k.k(\x[M])              [a->b] = ((a->b)'->o)->o
+    [MN] = \k.[M](\m.m[N]k)          [b] = (b'->o)->o
 
 Remember that types associate to the right.  Let's work through the
 application xform and make sure the types are consistent.  We'll have
@@ -227,14 +227,14 @@ the following types:
     M:a->b
     N:a
     MN:b 
-    k:b'->σ
-    [N]:(a'->σ)->σ
-    m:((a'->σ)->σ)->(b'->σ)->σ
-    m[N]:(b'->σ)->σ
-    m[N]k:σ 
-    [M]:((a->b)'->σ)->σ = ((((a'->σ)->σ)->(b'->σ)->σ)->σ)->σ
-    [M](\m.m[N]k):σ
-    [MN]:(b'->σ)->σ
+    k:b'->o
+    [N]:(a'->o)->o
+    m:((a'->o)->o)->(b'->o)->o
+    m[N]:(b'->o)->o
+    m[N]k:o 
+    [M]:((a->b)'->o)->o = ((((a'->o)->o)->(b'->o)->o)->o)->o
+    [M](\m.m[N]k):o
+    [MN]:(b'->o)->o
 
 Be aware that even though the transform uses the same symbol for the
 translation of a variable (i.e., `[x] = x`), in general the variable