Migratory Typing for Algebraic Effects and Handlers
Migratory Typing · Interoperability · Effect Handlers · Typed Racket · Runtime Contracts
Prototype implemented; formal semantics and proofs in progress.
Algebraic effect handlers separate a computation’s requests from their interpretation. A computation can request an operation, such as reading input or choosing between alternatives, while an enclosing handler determines how to respond and whether to resume the computation. An effect system statically describes which operations may escape a computation and require handling by its surrounding context.
These guarantees become harder to maintain when typed modules interact with untyped modules. A function declared to perform only input operations might call an untyped function that unexpectedly performs an output operation. Checking ordinary argument and result types does not detect this violation. Moreover, an effect request can pass through several function calls and module boundaries before reaching its handler.
My work investigates how to enforce effect specifications in this mixed setting of migratory typing. I am extending Typed Racket, which supports interoperability between statically typed and dynamically typed modules, with effect typing and runtime contracts. The project connects source-level effect guarantees with their realization using delimited continuations.
Core Contributions
1. Retrofitting effect typing into an existing typed language.
The prototype extends Typed Racket’s type checker to track both the values that expressions produce and the effects those expressions may perform. Function types describe the effects of calling a function; handler types describe the effects a handler handles, the result it produces, and the effects that may remain afterward.
This information must survive the existing compiler pipeline, including higher-order function calls, polymorphic instantiation, and module imports. The implementation integrates effect information into these mechanisms, allowing typed programs to check effectful computations while continuing to use Racket’s existing language infrastructure.
2. Runtime contracts that enforce escaping-effect specifications.
I implement contracts that monitor effect requests as they cross protected boundaries. For example, a function contracted to allow only a read effect is rejected if a write request escapes its execution, even when an outer handler could handle that request. Conversely, an operation handled entirely inside the function does not violate its external effect specification.
The central challenge is deciding which boundaries an operation actually crosses. Handler forwarding and continuation resumption complicate this task: resuming a suspended computation should not automatically attribute that computation’s effects to the handler implementation.
The contracts use Racket’s continuation mechanisms to maintain this distinction. Separate contract components check effect allowances and the values exchanged through operations and handlers. These contracts are available as a reusable library, while Typed Racket generates them from boundary types.
3. Effect declarations that work across module boundaries.
Effects must retain their identity when separately defined components interact. A handler imported from one module must recognize the same operation performed in another, including when imports are renamed or re-exported.
The prototype associates an effect declaration’s static information with its lexical binding and carries that information through Racket’s module system. This connects the operation known to the type checker with the operation recognized by the runtime, allowing effectful components to be organized and reused through ordinary module interfaces.
4. Effect-row polymorphism across typed/untyped boundaries.
Reusable higher-order functions often need to accommodate the effects of their arguments. For example, the same runner may invoke a callback that reads input or one that writes a log. Effect-row polymorphism expresses this relationship without fixing one effect allowance for every use.
The prototype supports explicit row instantiation and contracts for polymorphic functions crossing typed/untyped boundaries. Its current enforcement checks the concrete effect allowance selected at instantiation. This provides a foundation for, but does not yet establish, relational effect-row parametricity.
5. Ongoing formal work.
I am developing a high-level calculus for typed/untyped interaction with effect handlers and a lower-level calculus exposing the continuation and contract mechanisms used by the implementation. The intended results are type-and-effect soundness, together with a behavioral correspondence between the two levels.
A central next step is preserving effect-row abstraction across boundaries. Beyond checking a concrete set of permitted operations, this requires understanding how polymorphic code may generate, forward, or intercept effects belonging to an abstract row. The broader goal is a semantic specification that connects these abstraction guarantees to an executable implementation in an existing language.