Polarized Scheme: duality of computation, delimited control, and continuation-passing macro Interleaving

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