Implicit modules, a middle step towards modular implicits
summary
Claims a working implementation and formalization of modular implicits prototype for OCaml: a module-elaboration engine that synthesizes first-class module arguments from signatures, and a companion modular explicits change already slated for integration. It implements an incremental search state machine with reduction rules, constant-time candidate selection, shallow-subtyping filters, and a termination criterion based on a depth × ω metric over types. It is deterministic and sound but deliberately incomplete (rejects some terminating searches), and still needs work to integrate inference with core-language type inference.
AI-written summary · about
chapters (13)
- 0:00Missing features in Haskell OCaml
- 1:04Implicit modules introduction
- 2:28Module expressions in practice
- 4:13Soundness and inference determinism
- 6:43Completeness and termination criteria
- 9:15Multiple functor arguments and order
- 12:46Dynamic module resolution
- 20:35Implementation optimizations
- 21:37Future directions for implicit modules
- 23:01Q&A on scoping and termination
- 24:28Scala comparison and termination
- 25:55Implicit modules scoping rules
- 26:58Uniqueness and weakening property
related talks
24mOn the design and implementation of Modular Explicits
15mElaboration with First-Class Implicit Function Types
22mCounterexample-Guided Inference of Modular Specifications
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
15mType-safe generation of modules in applicative and generative styles
29mMechanized monadic equational reasoning for ML references
30mAnalyzing Programs with SMT Solvers
19mExtensible Metatheory Mechanization via Family Polymorphism