Chen, Xiao 陈骁

Languages that combine static and dynamic typing use different runtime enforcement strategies: some wrap values in contracts, some merge casts, and others insert shallow checks. These choices affect not only type safety but also which boundary violations are detected and whether blame identifies the responsible boundaries. Comparing these guarantees is difficult when each semantics is analyzed using different definitions and proof techniques.

My work develops Type as Obligations (TAO), a common framework for formalizing these guarantees. Its central idea is to distinguish what a program owes to its types from how a particular semantics enforces those requirements.

Previous work on vigilance provides a related perspective: values should respect their runtime typing histories, not merely their final types. However, vigilance characterizes this requirement through a logical relation indexed by a proof-level typing history, leaving blame outside its analysis. My framework reifies typing-history obligations into an explicit obligation store, maintained by an executable profiler semantics. This makes the propagation and violation of obligations directly inspectable and brings type enforcement and blame into the same analysis.

Core Contributions

1. A uniform, executable profiler semantics for type obligations.

I introduce a profiler semantics that records the typing history of values, i.e., the type-induced boundaries they have crossed. Type obligations originate at these typed–untyped boundaries and propagate through function arguments, results, and pair projections, including higher-order interactions where runtime proxies are created, merged, or discarded. This provides a common basis for defining obligation soundness and blame correctness independently of a particular enforcement mechanism.

The profiler also makes counterexamples operationally explainable. A language designer can execute a program and inspect which requirements were violated, how they reached the affected value, and whether the reported blame matches the violated obligations. This exposes enforcement failures even when ordinary evaluation returns successfully.

2. Mechanical construction of the profiler semantics, with a proof of bidirectional correspondence.

For ordinary semantics expressed through TAO’s common interface, TAO mechanically constructs the corresponding profiler semantics by intercepting reduction steps, inserting profiling commands at appropriate points, and delegating the computational reductions back to the ordinary semantics. Individual programs require no manual instrumentation; the framework determines where obligations must be recorded and propagated.

Moreover, I prove a bidirectional correspondence between ordinary and profiler evaluation. The correspondence accommodates additional obligation-bookkeeping steps and differences in allocated locations between the two semantics. In particular, a well-typed, uniquely labeled source program terminates with a resolved value in the ordinary semantics exactly when it terminates with that same value in the profiler semantics.

This bidirectional correspondence theorem justifies using the profiler semantics to reason about ordinary evaluation. On the one hand, “profiler evaluation implies ordinary evaluation” shows that the profiler faithfully simulates ordinary evaluation without introducing behavior, apart from additional obligation-bookkeeping steps. On the other hand, “ordinary evaluation implies profiler evaluation” ensures that the profiler captures ordinary evaluation without omitting behavior; such omissions would limit the conclusions drawn from the profiler. Thus, the profiler supports reasoning about the original semantics rather than replacing it with a different computation.

3. Obligation soundness: a new enforcement criterion that implies type soundness.

We propose obligation soundness for ordinary migratory typing semantics: throughout the profiler evaluation of any valid input program, no intermediate value may violate its type obligations. Although obligation soundness is a property of the ordinary semantics, it is defined using the type obligations recorded across all possible profiler evaluations. This definition is supported by the bidirectional correspondence theorem, which connects ordinary and profiler evaluation in both directions.

I prove that obligation soundness implies type soundness. The converse does not hold: a type-sound semantics may preserve a value’s final type while discarding that value’s typing history. This distinguishes returning a correctly typed result from respecting the requirements imposed throughout execution.

4. Blame correctness: a new ground truth for blame theorems.

We also propose a new criterion for blame theorems, using violated obligations as the ground truth for blame assignment.

An obligation violation represents an unfulfilled duty; its recorded boundary provenance identifies a candidate for blame. Accordingly, blame soundness means that blamed boundaries correspond to a subsequence of violated obligations, while blame completeness means that violated obligations correspond to a subsequence of the blamed boundaries. An ordinary semantics is blame correct if and only if it is both blame sound and blame complete.

5. A formal comparison of four enforcement strategies.

We apply TAO to four enforcement strategies for migratory typing: Natural, Threesomes, Forgetful, and Transient. Using the same property definitions, we establish both positive results and explicit counterexamples for the modeled semantics:

These results reveal substantive differences. Natural, a standard proxy-based strategy, enforces all type obligations and assigns blame correctly. Threesomes’ cast merging can report a conflict before an obligation is actually violated. Forgetful preserves result typing but loses obligation enforcement and blame completeness because it discards intermediate proxies. Transient does not use proxies to project untyped values or record their typing histories, which weakens its enforcement.

6. Mechanized metatheory and an executable model.

The framework, metatheory, and counterexamples are formalized in Rocq/Coq, with an accompanying executable Racket/Redex model. The broader contribution is a common semantic account that makes the guarantees of different enforcement strategies explicit, comparable, and machine-checked, while making their failures accessible through execution.

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 code interacts with untyped code. 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 accounting: 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 account that connects these abstraction guarantees to an executable implementation in an existing language.