Polymorphic Records for Dynamic Languages
summary
Extends semantic subtyping to support row polymorphism alongside union, intersection and negation types, defines a λ-calculus with record extension, selection and deletion, and proves type soundness. Provides decision algorithms: a subtyping procedure that only adds a finite-set containment check (so asymptotic cost stays the same) and a tallying algorithm for instantiating row variables that is sound but not complete. Implements ideas in the CIUS research language with planned Elixir integration and supports recursive types.
AI-written summary · about
chapters (7)
- 0:00Polymorphic records intro
- 1:27Semantic subtyping framework
- 6:51Core semantic subtyping idea
- 8:59Type checking with row polymorphism
- 11:48Typed lambda calculus
- 13:12Research summary
- 14:15Q&A
related talks
16mTowards Algebraic Subtyping for Extensible Records
28mTyping Records, Maps, and Structs
21mPolymorphic Type Inference for Dynamic Languages
48mA History of Subtyping
18mBackwards-Compatible Row-Based Exceptions in ML
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
19mMaking a Type Difference: Subtraction on Intersection Types as Generalized Recor...
19mMutually Iso-Recursive Subtyping