Typing first-class continuations in ML

TLDR

The paper examines extending ML with first‑class continuation primitives akin to those in Scheme. It defines a continuation‑based operational semantics for a small purely functional language, discusses alternative type systems, and provides programming examples. The study shows that the full Damas–Milner type system is unsound with first‑class continuations, but restricting polymorphism as in reference‑type systems restores soundness.

Abstract

Abstract An extension of ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are given. A continuation-based operational semantics is defined for a small, purely functional language, and the soundness of the Damas–Milner polymorphic type assignment system with respect to this semantics is proved. The full Damas–Milner type system is shown to be unsound in the presence of first-class continuations. Restrictions on polymorphism similar to those introduced in connection with reference types are shown to suffice for soundness.