On the design and implementation of Modular Explicits
summary
An OCaml compiler extension implements module-dependent functions that let functions take first-class modules and use module components in result types, fixing cases that were previously untypable. Implementation reuses the principal-types machinery from semi-explicit polymorphism and polymorphic methods, remains compatible with first-class modules, and supports applicative functors. Restrictions: parameters must be directly unpacked and applications must pack modules immediately; unification merges bound names with capture checks. A prototype branch is available to test. principal types preserved.
AI-written summary · about
chapters (12)
- 0:00Welcome
- 1:51Modular Explicits intro
- 2:36Motivation for Modular Explicits
- 4:02First-class modules limits
- 6:54Module-dependent functions
- 8:17Show module use case
- 9:24Type system challenges
- 11:51Unification and principal types
- 13:58Future work challenges
- 15:42Mod Implicit feature
- 17:05Conclusion
- 18:53Q&A
related talks
28mImplicit modules, a middle step towards modular implicits
28mSemi-explicit polymorphic parameters
19mExtensible Metatheory Mechanization via Family Polymorphism
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
15mType-safe generation of modules in applicative and generative styles
21mPolymorphic Type Inference for Dynamic Languages
21mTail Modulo Cons, OCaml, and Relational Separation Logic
17mUnboxed types for OCaml