These are some notes I gave out at one of my weekly recitations when I was teaching 15-312 Principles of Programming Languages at CMU in April 2017. Continuations have a fascinating analogy with proofs by contradiction that I might flesh out into a proper post in the future, but for now here are some rough recitation notes.
They’re best understood with Chapter 30 of Practical Foundations for Programming Languages open. (Unfortunately this chapter isn’t available in the online preview of the 2nd edition. I’m happy to lend you my hard copy if I know you IRL.)
Abstract:
Continuations allow for lots of things. Intuitively, we can think of continuations as “functions that never come back.” That is, continuations transfer control to some other part of your program. In a way, continuations are like a much nicer version of
goto. But they’re way more than this—specifically, they reify the concept of a “proof by contradiction” into the type system.