-[(\xy)(ww)] ~~>
-\k.[\xy](\m.m[ww]k) ~~>
-\k.[\xy](\m.m(\k.[w](\m.m[w]k))k) ~~>
-\k.[\xy](\m.m(\k.(\k.k(\x[xx]))(\m.m[w]k))k) ~~> beta*
-\k.[\xy](\m.m(\k.(\x[xx])[w]k)k) ~~>
-\k.[\xy](\m.m(\k.(\x(\k.[x](\m.m[x]k)))[w]k)k) ~~>
-\k.[\xy](\m.m(\k.(\x(\k.x(\m.mxk)))[w]k)k) ~~> beta
-\k.[\xy](\m.m(\k.[w](\m.m[w]k))k) --- same as second line!
+Thinking through the types
+--------------------------
+
+This discussion is based on [Meyer and Wand 1985](http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.44.7943&rep=rep1&type=pdf).
+
+Let's say we're working in the simply-typed lambda calculus.
+Then if the original term is well-typed, the CPS xform will also be
+well-typed. But what will the type of the transformed term be?
+
+The transformed terms all have the form `\k.blah`. The rule for the
+CBN xform of a variable appears to be an exception, but instead of
+writing `[x] => x`, we can write `[x] => \k.xk`, which is
+eta-equivalent. The `k`'s are continuations: functions from something
+to a result. Let's use σ as the result type. The each `k` in
+the transform will be a function of type ρ --> σ for some
+choice of ρ.
+
+We'll need an ancilliary function ': for any ground type a, a' = a;
+for functional types a->b, (a->b)' = a' -> (b' -> o) -> o.
+
+ Call by name transform
+
+ Terms Types
+
+ [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
+the following types:
+
+ M:a->b
+ N:a
+ MN:b
+ k:b'->o
+ [N]:a'
+ m:a'->(b'->o)->o
+ m[N]:(b'->o)->o
+ m[N]k:o
+ [M]:((a->b)'->o)->o = ((a'->(b'->o)->o)->o)->o
+ [M](\m.m[N]k):o
+ [MN]:(b'->o)->o
+
+Note that even though the transform uses the same symbol for the
+translation of a variable, in general it will have a different type in
+the transformed term.