Polymorphic Type Inference for Dynamic Languages
summary
Claims a type system that combines first‑order polymorphism with intersection, union and semantic subtyping and proves safety; it gives unannotated functions Hindley‑Milner polymorphic yet overloaded types and supplies a sound and terminating reconstruction algorithm that nevertheless requires annotation hints and uses tallying and backtracking to solve subtype constraints. Implementation in OCaml is available as an online demo and artifact archive; the algorithm applies union‑elimination exactly once per distinct subexpression via maximal‑sharing canonical form, but subtyping can be exponential and inference can blow up without user annotations.
AI-written summary · about
chapters (8)
- 0:00Polymorphic type inference intro
- 1:27Set-theoretic types for dynamic langs
- 3:56Declarative type system building
- 7:29Intersection and union type rules
- 9:14Expression transformation for typing
- 10:37Annotation inference with tallying
- 13:03Implemented system summary
- 14:23Q&A
related talks
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
21mOmnidirectional type inference for ML
28mSemi-explicit polymorphic parameters
15mPolymorphic Records for Dynamic Languages
15mA compilation method for dynamic typing in ML
19mExtensible Metatheory Mechanization via Family Polymorphism
56mOn Type-Based Techniques for Program Manipulation
30mOn Distributive Subtyping with Finitary and Infinitary Unions and Intersections