Observing Definitional Equality
summary
Proposes replacing the usual dependent observational equality used in heterogeneous unification (Gundry, McBride, Juan) with homogeneous observational equality from Pujet and Tabareau, claiming simpler elaboration and more solutions; describes a working prototype implementation in progress that uses normalization by evaluation and a spine-based neutral representation, requires three coercion representations, and confronts production issues: eager reflexive-coercion reduction, short/coercion-on-neutrals handling, and coercing inductive indices; argues undecidable looping only occurs with inconsistent meta contexts and suggests combining homogeneous and heterogeneous modes.
AI-written summary · about
chapters (18)
- 0:00Observing definitional equality
- 0:21Unification with sigma types
- 1:47Dependent type unification
- 3:15Existing solutions drawbacks
- 4:20Postponed equality observational
- 6:27Partial vs total core
- 7:51Reflexive coercions issues
- 9:40Short coercions for strength
- 11:51Coercions via normalization
- 13:37Coercion representation cases
- 16:07Coercing inductive types
- 18:40Alternative approaches burden
- 19:43Undecidability of coercion
- 21:52Heterogeneous unification
- 23:17Further work challenges
- 23:58Q&A pattern matching
- 25:04Meta context failures
- 26:53Q&A coercion terms
related talks
26mObservational Equality: Now for Good
23mImpredicative Observational Equality
17mBetter Together: Unifying Datalog and Equality Saturation
14mAdequacy for Algebraic Effects Revisited
59mUnification Modulo Equational Theories in Languages with Binding Operators
21mChecking Equivalence in a Non-strict Language
19mTowards Relational Contextual Equality Saturation
19mA Dependently Typed Language with Dynamic Equality