Backwards-Compatible Row-Based Exceptions in ML
summary
Type system extends ML with row polymorphism and a new top row to make exception tracking backwards compatible, proving that unannotated code types as top-row and that refined exception types are subtypes of original ones (graceful generalization). It models local exceptions, higher-order refs, polymorphism and concurrency, gives safety and representation-independence via binary logical relations in a relational separation logic, and is mechanized in Rocq + Iris with examples from OCaml stdlib, Jane Street, and Filinski.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 1:26Row-based exception tracking
- 3:53Backwards compatibility
- 8:05Precise tracking via rank polymorphism
- 12:44Representation independence
- 14:58Safety guarantees
- 15:19Conclusion
related talks
15mPolymorphic Records for Dynamic Languages
21mOmnidirectional type inference for ML
31mRethinking the Value Restriction
27mDesigning interrupts for ML and OCaml
16mTowards Algebraic Subtyping for Extensible Records
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
29mMsML: A Proposal for a successor ML
21mPolymorphic Type Inference for Dynamic Languages