Gradual Typing for Effect Handlers
summary
GrEff is a gradually typed language for effect handlers that supports incremental migration from unchecked to checked effect typing; it elaborates to a cast calculus called Core GrEff, adds explicit value and effect casts, and models runtime type errors. The work gives an equational theory that yields an operational semantics, and proves soundness and the graduality theorem via an operational logical-relations model (extending embedding–projection pair techniques). No implementation yet, but the metatheory validates that checked, unchecked, and mixed modules interoperate and that errors move predictably from runtime to compile time.
AI-written summary · about
chapters (14)
- 0:00Gradual typing intro
- 1:05Effect typing terms
- 2:06Design goals for gradual effects
- 2:47Unchecked effect tracking
- 4:30Migrating to checked effects
- 7:00Gradual typing overview
- 8:02Graff language design
- 10:08Graff core calculus
- 11:10Equational theory in Graff
- 12:14Term precision
- 13:19Handler equational principles
- 14:23Soundness and graduality
- 15:28Future work
- 15:49Summary and Q&A
related talks
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
15mEffects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism
40mGradualizer: challenges implementing a type checker
16mGradually Typing Strategies
18mSpace-Efficient Polymorphic Gradual Typing, Mostly Parametric
46mThe Calculated Typer (Functional Pearl)
16mA Type-and-Effect System for Object Initialization
15mEfficient Compilation of Algebraic Effect Handlers