Notes on Continuations

June 18, 2019

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.)

→ Continuations

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.

Read More

Sorbet Does Not Have FixMe Comments

Sorbet has no way to ignore an error on a specific line with a magiccomment. This is different from all other gradual static type checkers …… Continue reading

What makes type checking Ruby hard?

Published on December 29, 2019