Continuations continued

Simulating effects in CPS

Previously, we saw that the CPS translation of a term becomes a function that takes a continuation k and either passes a value to k or evaluates the CPS translation of a subterm using continuation k. In this final section, we look at what happens when we make the CPS translation of a term do something different.

Consider again the example term

+ (* 3 3) (* 4 4)

which we convert into CPS (doing less simplification than before) as

λk. (λk₁. *' 3 3 k₁) (λv₂. *' 4 4 (λv₃. +' v₂ v₃ k))

Let’s focus on the subterm (λk₁. *' 3 3 k₁).

Exceptions

If we replace this subterm with something that ignores k₁, like λk₁. * 3 3 (note: not *'), and apply everything to a final continuation exit, we get:

λk. (λk₁. * 3 3) (λv₂. *' 4 4 (λv₃. +' v₂ v₃ k)) exit
⟶ (λk₁. * 3 3) (λv₂. *' 4 4 (λv₃. +' v₂ v₃ exit))
⟶ * 3 3
⟶ 9

The + [·] (* 4 4) was thrown away, and 9 became the final answer. We can use a similar mechanism to simulate error without try:

𝒞⟦error⟧ = λk. exit <err=unit>

Additionally, we stipulate that the final continuation be λv. exit <ok=v>. Then a term will either evaluate to exit <ok=v> for some v, or exit <err=unit>.

For example:

𝒞⟦+ error (* 4 4)⟧ (λv. exit <ok=v>)
  = λk. (λk₁. exit <err=unit>) (λv₂. *' 4 4 (λv₃. +' v₂ v₃ k)) (λv. exit <ok=v>)
⟶ (λk₁. exit <err=unit>) (λv₂. *' 4 4 (λv₃. +' v₂ v₃ (λv. exit <ok=v>)))
⟶ exit <err=unit>

To add try t₁ with t₂, we evaluate the CPS translation of t₁, but we don’t pass it the current continuation:

𝒞⟦try t₁ with t₂⟧ = λk. case 𝒞⟦t₁⟧ (λx. <ok=x>) of
                          <ok=v> ⇒ k v,
                          <err=u> ⇒ 𝒞⟦t₂⟧ k

Instead of passing the current continuation k, we pass it λx. <ok=x>, similar to the final continuation we used above. Instead of making this the final answer, we check what kind of value it is; if it’s <ok=v>, we pass v to the continuation k, but if it’s <err=u>, we pass the continuation to the handler 𝒞⟦t₂⟧.

If we assume there are no uncaught exceptions, we can let the final continuation again be exit.

Question: The above translation no longer has the property that every call is a tail call, because the application 𝒞⟦t₁⟧ (λx. <ok=x>) is not in the tail position of the case expression. Does this mean that in order to use one benefit of CPS (implementing control), we had to trade away another (every call is a tail call)?

Finally, to change error into raise:

       𝒞⟦raise v⟧ = λk. <err=𝒞_v⟦v⟧>
𝒞⟦try t₁ with t₂⟧ = λk. case 𝒞⟦t₁⟧ (λx. <ok=x>) of
                          <ok=v> ⇒ k v,
                          <err=v> ⇒ 𝒞⟦t₂ v⟧ k

Nondeterminism

The “opposite” of a CPS term that ignores its continuation is one that uses its continuation twice or more. Returning to our running example, what if we replace (λk₁. *' 3 3 k₁) with (λk₁. [k₁ 100, k₁ 200])?

λk. (λk₁. [k₁ 100, k₁ 200]) (λv₂. *' 4 4 (λv₃. +' v₂ v₃ k)) exit
⟶ (λk₁. [k₁ 100, k₁ 200]) (λv₂. *' 4 4 (λv₃. +' v₂ v₃ exit)) 
⟶ [(λv₂. *' 4 4 (λv₃. +' v₂ v₃ exit)) 100, (λv₂. *' 4 4 (λv₃. +' v₂ v₃ exit))  200]
⟶* [116, 216]

We can do something similar to simulate nondeterminism:

     𝒞⟦amb v⟧ = λk. concat (map k 𝒞_v⟦v⟧)
 𝒞⟦collect t⟧ = λk. k (𝒞⟦t⟧ (λx. [x]))

Generators

Yet another possibility is for a CPS term to wrap its continuation inside an abstraction:

λk. (λk₁. λx. k₁ x) (λv₂. *' 4 4 (λv₃. +' v₂ v₃ k)) exit
⟶ (λk₁. λx. k₁ x) (λv₂. *' 4 4 (λv₃. +' v₂ v₃ exit))
⟶ λx. (λv₂. *' 4 4 (λv₃. +' v₂ v₃ exit)) x

The term now evaluates to an abstraction; if we apply this abstraction to avalue 9, the computation resumes with that value:

(λx. (λv₂. *' 4 4 (λv₃. +' v₂ v₃ exit)) x) 9
⟶ (λv₂. *' 4 4 (λv₃. +' v₂ v₃ exit)) 9
⟶ *' 4 4 (λv₃. +' 9 v₃ exit)
⟶* exit 25

We can do something similar to simulate generators:

  C⟦gen t⟧ = λk. k (C⟦t⟧ (λr. <stop=r>))
C⟦yield v⟧ = λk. <next={𝒞_v⟦v⟧, λi. λk'. k' (k i)}>

State

We can even use this trick to simulate a mutable state. Apply our running example term to the final continuation (λx. λs. exit {x, s}):

λk. (λk₁. *' 3 3 k₁) (λv₂. *' 4 4 (λv₃. +' v₂ v₃ k)) (λx. λs. exit {x, s})
⟶* λs. exit {25, s}

If we apply this to an initial state (say, 100), we get {25, 100}, the result of the computation and the final (unchanged) state.

Now change (λk₁. *' 3 3 k₁) to (λk₁. λs. k₁ s s):

λk. (λk₁. λs. k₁ s s) (λv₂. *' 4 4 (λv₃. +' v₂ v₃ k)) (λx. λs. exit {x, s}) 100
⟶ (λk₁. λs. k₁ s s) (λv₂. *' 4 4 (λv₃. +' v₂ v₃ (λx. λs. exit {x, s}))) 100
⟶ (λs. (λv₂. *' 4 4 (λv₃. +' v₂ v₃ (λx. λs. exit {x, s}))) s s) 100
⟶ (λv₂. *' 4 4 (λv₃. +' v₂ v₃ (λx. λs. exit {x, s}))) 100 100
⟶ *' 4 4 (λv₃. +' 100 v₃ (λx. λs. exit {x, s})) 100
⟶* (λs. exit {116, s}) 100
⟶ exit {116, 100}

What happened? The CPS term (λk₁. λs. k₁ s s) wrapped up the continuation into an abstraction looking for the current state, 100. Then k s resumes the computation with 100 as the value of the first addend. But k s is going to look for the state again, and we’ve just consumed it. So we need to re-apply k s to the current state.

Now change (λk₁. *' 3 3 k₁) to (λk₁. λs. k₁ 9 200):

λk. (λk₁. λs. k₁ 9 200) (λv₂. *' 4 4 (λv₃. +' v₂ v₃ k)) (λx. λs. exit {x, s}) 100
⟶* (λs. exit {25, s}) 100
⟶ exit {25, 100}

This time, the CPS term (λk₁. λs. k₁ 9 200) consumes the initial state 100 and discards it. It applies k to 9, making it the value of the first addend, and then to 200, which becomes the new value of the state.

More generally, we can simulate a cell of mutable state like this:

   𝒞⟦set v⟧ = λk. λs. k unit 𝒞_v⟦v⟧
𝒞⟦get unit⟧ = λk. λs. k s s

Simulating effects in direct style

So a wide range of effects can be simulated in CPS. What if you hate CPS? That’s okay – you don’t have to write in it, because the computer can translate your code into CPS for you.

No, what if you really hate CPS and want to define new effects without having to define their translation into CPS? That’s okay too – it turns out that there are effects that are versatile enough to simulate all of the effects we’ve seen:

One of them you’ve seen already: gen and yield can be used to simulate exceptions, nondeterminism, mutable state, and other effects.
If resumable exceptions are defined in the right way, they also can simulate the other effects we’ve seen. (This is quite closely related to what are called effect handlers.)
The operators shift and reset, which we haven’t seen.
Scheme’s call-with-current-continuation (call/cc for short) can’t, but in conjunction with mutable state, it can simulate the other effects.