Continuation-PassingStyle

Or, how to travel through time!

Michael Arntzenius (rntz)

CPS is a technique, but also more than that.

exciting b/c connected to so many things!

"microcosm of CS".

What is CPS?

BORING!

It's just higher-order functions.

BIZARRE!

It's programs playing with their own futures!

A manual version of call/cc —"the mother of all control flow constructs"!

Connects classical and constructive logic!

Simplifies compiler optimizations —a functional version of SSA!

The Tiniest Regexp Library!

data Re = Lit Char | Seq Re Re | Or Re Re | Star Re

match (Lit c) [] k = False
match (Lit c) (x:xs) k = c == x && k xs
match (Seq a b) s k = match a s (\rest -> match b rest k)
match (Or a b) s k = match a s k || match b s k
match (Star a) s k = match a s (\rest -> match (Star a) rest k) || k s

matches a s = match a s null

{Haskell, Python} code at https://github.com/rntz/cps-talk

CPS by example. Backtracking search.

New technique in 10min, sucker's game.

The gist of CPS

matches :: Regexp -> String -> Bool

matchBetter :: Regexp -> String -> Maybe String

matchBest :: Regexp -> String -> [String]

match :: Regexp -> String -> (String -> Bool) -> Bool
--                           ^ CONTINUATION ^

Directly writing matches, prefix problem.

Generalize to give "maybe suffix"; multiple matches problem.

Generalize to give "suffix list"; iterator/lazy problem.

There is another way!

What's the big deal?

What's the big deal?

There isn't one.

What if you wroteevery function in CPS?

If every function were CPS...

Every function could manipulate its own future! You could:

• Continue multiple times! Multiple choice futures!
• Continue from an earlier function! Early exit! Exceptions!
• Switch back and forth between continuations!Generators! Coroutines! Threads!

Remember call/cc?

Curry-Howard and CPS

If proofs are programs, what does call/cc prove?

If CPS transforms programs, what does it do to proofs?

What does time travel mean in a proof?