Semi-explicit polymorphic parameters
summary
Reuses Garrigue and Remy’s semi-explicit ideas to add labeled types for polymorphic parameters, gives formal typing rules and implements them in an OCaml branch by treating arrow constructors as mutable arrow constructors and tracking levels for generalization, so instantiation side-conditions are decidable. Prototype-to-production took about six hours and the feature has run at Jane Street for almost a year with no reported problems, supporting polymorphic parameters annotated at lambdas while preserving inference elsewhere.
AI-written summary · about
chapters (14)
- 0:00Semi-explicit polymorphic parameters
- 1:44Core idea from PolyML
- 3:10Type grammar for polymorphism
- 5:17Introduction rule
- 8:04Elimination rule challenge
- 10:31Labeled types solution
- 12:57Type annotations handling
- 14:01OCaml implementation
- 16:27OCaml integration
- 17:07Approach limitations
- 18:54Higher-rank polymorphism
- 19:37First-class polymorphism
- 21:22Summary and impact
- 21:43Q&A
related talks
21mPolymorphic Type Inference for Dynamic Languages
20mGenerating Well-Typed Terms that are not "Useless"
24mOn the design and implementation of Modular Explicits
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
18mSpace-Efficient Polymorphic Gradual Typing, Mostly Parametric
43mAdding kind-polymorphism to the Scala programming language
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml
15mElaboration with First-Class Implicit Function Types