Principal Type Inference under a Prefix: A Fresh Look at Static Overloading
summary
A new rule set, HMQ (type inference under a prefix), replaces HM guessing with fresh type variables plus composable prefixes as solvable constraints, yielding always-principal types that correspond to Algorithm W results; unification and a gen-sub rule implement prefixes via substitutions. The paper shows how FreezeML/HMF style restrictions disappear and describes static overloading implemented in Koka, arguing the approach is algorithmically simple, compatible with practical W-style algorithms, and works on the examples presented (formal correspondences left for future proofs).
AI-written summary · about
chapters (13)
- 0:00Principal type inference intro
- 1:03Hindley-Milner limitations
- 5:02Static overloading challenges
- 8:14Predicative extensions problems
- 11:45HMQ type rules intro
- 12:31HMQ improvements
- 13:14HMQ rules structure
- 14:59Prefixes in HMQ
- 16:04HMQ unification rules
- 17:07HMQ gen-sub rules
- 17:48Static overloading with HMQ
- 18:08HMQ advantages and future
- 18:31Q&A
related talks
21mPolymorphic Type Inference for Dynamic Languages
21mOmnidirectional type inference for ML
32mMLstruct: Principal Type Inference in a Boolean Algebra of Structural Types
15mThe Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
15mThe Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with(…)
24mDecoupling Resolution from Type Inference
16mPolymorphic Types and Effects with Boolean Unification