Continuations and Coexponentials
summary
Proposes that higher-order continuations are categorical coexponentials and shows how the continuation monad and a full-image factorization of negation produce a Kleisli/Kleisli-style adjunction that yields Lambda bar and derives call/cc and other control operators. Presents a typed language combining exponentials and coexponentials with a value restriction to avoid collapse, gives a complete equational theory (beta and control equations), demonstrates examples (excluded middle, short-circuit multiply with no extra traversal) and an ML implementation on GitHub.
AI-written summary · about
chapters (13)
- 0:00Welcome
- 0:29Duality in programming
- 4:48Semantics of continuations
- 9:48Loch Ness semantics
- 11:57Designing a programming language with co-exponentials
- 13:20Natural deduction for continuations
- 17:40Algebra of functions
- 19:08Programs with continuations
- 22:57Control effects
- 24:44Speculative evaluation
- 26:12Applications on continuations
- 27:39Summary
- 28:00Q&A
related talks
36mParallel Algebraic Effect Handlers
16mS4 modal sequent calculus as intermediate logic and intermediate language (Short Paper)
36mDependently Typed Multi-Stage Programming, Revisited
15mLatent Effects for Reusable Language Components
45mA categorical view of computational effects
08mLightning Talk: Designing a Language for Learning Continuations
34mAn introduction to Lambda Calculus
24mClassical Notions of Computation and the Hasegawa-Thielecke Theorem