Implementing Dependent Pattern Matching and Type Unification Part 2
summary
A small dependently typed core is extended with telescopes, closures and a datatype registry that compiles clauses into case trees; an elaborator builds constraints per-argument and repeatedly splits on data constructors to produce nested cases. Equality is treated specially via type-directed unification that returns success, refutation or undecided; this lets the compiler validate forced and absurd patterns and prune impossible branches. The implementation type-checks examples like addition and vector append but can conservatively fail coverage checking when undecidable.
AI-written summary · about
chapters (10)
- 0:00Data Types, Parameters, And Indices
- 8:10Encoding Indexed Types With Equality
- 10:18Telescopes And Type Checking
- 20:04Introduction To Dependent Pattern Matching
- 41:17From Pattern Matching To Case Trees
- 48:21Elaborating Clauses Into Case Trees
- 58:55Splitting On Data Constructors
- 1:10:23Dependent Pattern Matching And Unification
- 1:18:13Unification Rules And Equality Constraints
- 1:23:34Coverage Checking And Future Extensions
related talks
23mType-Level Programming with Match Types
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
30mConstraint Typing with Boolean Algebra
19mA Dependently Typed Language with Dynamic Equality
29mUnification Modulo Isomorphisms between Dependent Types for Type-based Library Search
46mThe Calculated Typer (Functional Pearl)
26mType Narrowing the Hard Way
01h 03mVerifying Dependent Type-checkers