Towards Algebraic Subtyping for Extensible Records
summary
Extends Simple-sub to support extensible records by adding row variables to the type language and a concrete row expansion step in the constraint solver, reworking record typing and subtyping (unfold/ignore rules) so selection and extension stay well typed. The algorithm preserves decidability of type inference and still infers compact principal types without the heavy algebraic machinery of MLsub, and the modifications aim for an efficiently implementable inference pass.
AI-written summary · about
chapters (10)
- 0:00Start
- 0:28Background
- 1:54Algebraic subtyping in MLsub
- 2:56Algebraic subtying and records
- 4:18Algebraic subtyping and record extension
- 6:12Extending MLSub with row polymorphism
- 7:33New record typing rules
- 8:24Subtyping relation
- 9:47Type inference concepts
- 10:57Type inference example
related talks
15mPolymorphic Records for Dynamic Languages
15mThe Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...
28mTyping Records, Maps, and Structs
48mA History of Subtyping
26mThe Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic(…)
18mBackwards-Compatible Row-Based Exceptions in ML
19mMutually Iso-Recursive Subtyping
19mMaking a Type Difference: Subtraction on Intersection Types as Generalized Recor...