Eta conversion for the unit type (is still not that simple)
summary
Argues that eta for unit needs type-directed conversion and proposes a bidirectional elaboration core interleaved with normalization-by-evaluation that computes types only on demand. Targets Agda’s shortcomings (current support is slow and incomplete) and aims to guarantee unique solutions of unification problems by detecting irrelevant/unfoldable contexts, refusing meta-solutions in irrelevant contexts, and bubbling failures into successes when guarded by irrelevance. Prototype uses lazy relevance annotations, optional memoization of relevance checks, and is partially implemented but not yet benchmarked.
AI-written summary · about
chapters (10)
- 0:00Eta conversion intro
- 1:51Unit eta in type theory
- 4:02Bidirectional elaboration setup
- 6:31Lazy types in evaluation
- 9:00Conversion with irrelevant types
- 11:52Optimizing relevance computation
- 16:11Advanced optimizations trade-offs
- 18:19Meta variables with unit eta
- 22:54Proposed approach summary
- 23:37Q&A on algorithm overhead
related talks
15mElaboration with First-Class Implicit Function Types
13mA Simpler Encoding of Indexed Types
35mPractical Normalization by Evaluation for EDSLs
25mShallowly embedding type theories
52mType Theory and its Meaning Explanations
19mIll-Typed Programs Don't Evaluate
46mThe Calculated Typer (Functional Pearl)
43mReuniting the familly with Eta: Haskell on the JVM