Elaboration with First-Class Implicit Function Types
summary
Presents an elaboration algorithm that actually inserts implicit lambdas by extending core Martin-Löf type theory with strictly curried function types and using meta variables to represent unknown insertions. It supports full dependent types, global inference, and a single-pass traversal with no backtracking, improves Agda-style bidirectional elaboration, and fixes cases like storing polymorphic functions in data (e.g. Maybe (∀a. a -> a)) where previously explicit implicit lambdas were required; application insertion remains future work.
AI-written summary · about
chapters (10)
- 0:00Start
- 2:12First-class implicit functions
- 3:28Impredicative polymorphism
- 4:04Contributions
- 4:43Basic Bidirectional Elaboration
- 6:17Implicit insertion (applications)
- 7:57Implicit insertion (lambdas)
- 9:10What can go wrong
- 10:13Solution
- 12:30Intermediate Core Theory
related talks
28mImplicit modules, a middle step towards modular implicits
20mGenerating Well-Typed Terms that are not "Useless"
30mDotty and types: the story so far
31mDependent tagless final
19mType Inference Logics
28mSemi-explicit polymorphic parameters
25mShallowly embedding type theories
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)