Extensible Data Types with Ad-Hoc Polymorphism
summary
Combines row polymorphism and type classes to let rows carry constraints like all constraint and to fold over fields with a new primitive end induction, while resolving non-determinism by making commutativity user-controlled (commutative vs non‑commutative rows). Formalizes the source calculus λ^{⇒}_{ρ} and elaborates to F^{⊗⊕}_{ω}, proves type safety and sound elaboration with mechanized proofs in Lean 4 proof, and evaluates the design on the Brown Benchmark with reusable artifacts.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:02Background on extensible types
- 3:50Row constraints for field access
- 5:35Row constraints for field updates
- 7:01Extensible types with type classes
- 8:46Generic boilerplate for records
- 10:12Generic type class instances
- 12:59Commutativity in row types
- 16:50Fixing non-determinism
- 17:11Induction primitive
- 20:04System summary
- 21:49Q&A