Chen, Xiao 陈骁

When typed and untyped modules interact, runtime enforcements must determine which type requirements to preserve and which boundaries to blame when those requirements fail. Different strategies use contracts, merge casts, or insert shallow checks, making their guarantees difficult to compare. Type soundness alone does not capture whether a value respects its typing history, i.e., every type requirement it encounters during execution.

Type as Obligations (TAO) makes these requirements explicit. Given an ordinary semantics, TAO will mechanically construct a corresponding profiler semantics. In addition to ordinary computation steps, the profiler semantics records each value’s typing history as type obligations, including their boundary origins, and propagates them through function calls and pair projections. This separates the requirements imposed by types from the runtime strategies to enforce them, giving different semantics a common basis for analysis.

My contributions connect this runtime profiling to formal guarantees:

• Mechanical profiler semantics with evaluation correspondence. For any ordinary semantics, 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. I prove a bidirectional correspondence between the ordinary and profiler evaluations.
• A stronger enforcement criterion. I define obligation soundness and prove that it implies type soundness, but not conversely: returning a correctly typed result does not ensure that every accumulated obligation was respected.
• Obligation-based blame criteria. The framework defines blame soundness and completeness using violated obligations and their boundary provenance as the reference for blame assignment.

I have applied these definitions to modeled versions of Natural, Threesomes, Forgetful, and Transient, proving positive results and exhibiting counterexamples. The framework, metatheory, and counterexamples are formalized in Rocq/Coq, with an executable Racket/Redex model. This comparison makes differences in enforcement and blame explicit and their causes inspectable through execution.

An effect system describes which operations may escape a computation and require handling by its surrounding context. This guarantee becomes difficult to preserve when typed and untyped modules interact. An untyped function can return a correctly typed value while performing an unexpected effect, and a request may cross several calls and module boundaries before reaching a handler.

Effect-Typed-Racket investigates this problem by extending Typed Racket with polymorphic algebraic effect handlers, effect typing, and runtime contracts. The central idea is to enforce effect specifications by monitoring the requests that escape protected computations. The implementation connects source-level effect information to runtime checks built using Racket’s delimited continuations.

My contributions connect source-level effect specifications to runtime enforcement:

• Effect typing within Typed Racket. Function types describe the effects of calls; handler types describe handled operations, result types, and remaining effects. I integrate this information into higher-order calls, polymorphic instantiation, and module imports, allowing effectful programs to use Typed Racket’s existing language infrastructure.
• Contracts for escaping effects. A function contracted to allow only read is rejected if a write request escapes its execution, even if an outer handler could handle it. An operation handled entirely inside the function does not violate its external effect allowance. These reusable contracts separately check effect allowances and the values exchanged through operations and handlers; Typed Racket generates them from boundary types.
• Effect identity across modules. I associate effect declarations’ static information with their lexical bindings, so the type checker and runtime handlers recognize the same operations across renamed imports and re-exports. This allows effectful components to be organized and reused through ordinary module interfaces.
• Effect-row polymorphism across typed–untyped boundaries. A higher-order function can accommodate callbacks with different effects, such as reading input or writing a log. The prototype supports explicit row instantiation and contracts that check the concrete effect allowance selected at each instantiation.

The prototype has been implemented. I am developing a high-level calculus for typed–untyped interaction with effect handlers and a lower-level calculus exposing the implementation’s continuation and contract mechanisms. The intended results are type-and-effect soundness and a behavioral correspondence between the two levels, connecting source-level guarantees to the executable implementation.