Typing Records, Maps, and Structs
summary
Proposes a type theory that unifies struct-style and map-style records with union, intersection, and negation types, models record values as quasi-constant functions, and defines semantic subtyping so T1 ≤ T2 reduces to emptiness checks. Delivers a proved-correct, backtracking-free subtyping algorithm, a calculus with selection/concatenation/deletion, and a canonical representation for record types used to implement selection and other type operators. Implementation is underway in Elixir and proposed for Ballerina.
AI-written summary · about
chapters (9)
- 0:00Records, maps, and structs
- 1:29Unified typing motivation
- 3:35Calculus and operations
- 8:15Type constructors and fields
- 12:12Subtyping and operators
- 19:27Union and intersection types
- 22:38Airline Maps operators
- 23:21Conclusion and future work
- 24:27Q&A
related talks
15mPolymorphic Records for Dynamic Languages
48mA History of Subtyping
16mTowards Algebraic Subtyping for Extensible Records
19mMaking a Type Difference: Subtraction on Intersection Types as Generalized Recor...
19mIll-Typed Programs Don't Evaluate
46mThe Calculated Typer (Functional Pearl)
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
30mConstraint Typing with Boolean Algebra