Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search
summary
Claims an equational unification procedure modulo a set of type isomorphisms for dependent product/sum types and presents a semi-algorithm plus a prototype implementation that actually finds meta-substitutions making query and candidate types isomorphic. Implementation uses normalization (reduction system R), nondeterministic decomposition with reordering, pruning of meta-arguments and meta-variable guessing. It solves real examples quickly on a tiny corpus (38 definitions tested) but behaves exponentially in branching so it currently targets local search and returns unifiers without isomorphism proofs.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 2:13Limitations of simple type comparison
- 4:03Key flexibilities in type-based search
- 6:37Unification modulo isomorphism approach
- 9:27Isomorphisms for dependent types
- 11:18Unification procedure by example
- 16:45Unification rules and simplification
- 21:04Pruning and meta-variable handling
- 23:57Implementation details
- 24:38Conclusion and future work
- 25:42Q&A
related talks
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
21mPolymorphic Type Inference for Dynamic Languages
59mUnification Modulo Equational Theories in Languages with Binding Operators
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
56mOn Type-Based Techniques for Program Manipulation
15mLiberating Merges via Apartness and Guarded Subtyping
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
15mThe Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...