Rethinking the Value Restriction
summary
Reformulates ML core with references and the value restriction and shows two standard assumptions fail: prenex polymorphism and let polymorphism are unsound once fresh references or exception types create hidden sharing. Proposes full rank‑1 subsumption, lazy instantiation of for‑alls at use and generalization only at lambdas, dropping the syntactic “value” check. Types a few extra examples (functions packaged with refs, polymorphic returns) and matches implementations like SML#/MLScript without changing runtime behavior.
AI-written summary · about
chapters (8)
- 0:00Hindley-Milner foundations
- 5:16The value restriction issue
- 7:11Rethinking the standard rules
- 15:02Lazy instantiation strategy
- 16:50Generalization in full rank
- 20:50Q&A on type system design
- 23:34Polymorphism for constructors
- 24:11Refining the implementation
related talks
29mMechanized monadic equational reasoning for ML references
29mMsML: A Proposal for a successor ML
14mThe Simple Essence of Monomorphization
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
15mThe Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...
15mSignature restriction for polymorphic algebraic effects
18mBackwards-Compatible Row-Based Exceptions in ML
21mOmnidirectional type inference for ML