Polarized Scheme unifies computation control and macros with type theory
Polarized Scheme: duality of computation, delimited control, and continuation-passing macro Interleaving
Programming Languages
Summary
Programming languages like Scheme have different ways to check types and handle advanced features like control flow. The authors introduce Polarized Scheme, which uses ideas from type theory to treat program values and their continuation contexts as dual entities, allowing clean and symmetric handling of functions and control operations. They also show how macros can be understood as interleaved sequences of continuations, integrating expansion and evaluation. Their approach is backed by formal proofs and a verified implementation.
What this means in practice
- •For programming language implementers: Design static type systems that symmetrically handle values and continuations, enabling safe and modular control flow features like shift/reset.
- •For macro system developers: Construct hygienic macro systems that integrate macro expansion and evaluation via a continuation-passing pipeline for better correctness and modularity.
A theory result. No direct application yet.
Authors
Christopher Dutchyn
Abstract
Static type systems for Scheme have traditionally followed one of two paths: manifest type checking with multi-dispatch (Clifton and Leavens, 2005) or latent occurrence typing tailored for untyped interoperation (Tobin-Hochstadt and Felleisen, 2008). In this paper, we propose Polarized Scheme, a static foundation built upon polarized type theory and the duality of computation. In Polarized Scheme, values are positive data producers (A+) and continuations are negative observation consumers (~A+). Functions operate symmetrically under dual viewpoints: as forward value-transformers and as backward continuation-transformers. Computation exists exclusively at the interaction cut <P|K> executed on a focus-and-context abstract machine separating positive data focus from negative return contexts (R). Delimited control (shift/reset) and continuation marks are expressed directly as Return Stack frame operations parameterized by the prompt's ambient answer type without polluting producer data types. Furthermore, we formalize the hygienic macro system as an interleaved continuation-passing pipeline, where macro expansion erects its own continuation hierarchy nesting into runtime evaluation. We prove Subject Reduction, Progress with respect to prompt-delimited stacks, prove Duality Bisimilarity, characterize Return Stack reclamation for dynamic closures, and report on an executable reference implementation in a verified dialect of Go with a verified cut-elimination dispatcher