Type Checking with Rewriting Rules
summary
Claims that recursive type-class constraints are undecidable are addressed by encoding constraints as term rewriting rules and using Knuth-Bendix completion to semi-decide type equalities. The implementation in Hylo normalizes encoded types to answer equality and conformance queries, uses prefix trees to find overlaps for performance, and enforces a pragmatic 1,000-rule cutoff so compilation terminates; it succeeds on real code but remains inherently semi-decidable and can reject overly complex trait signatures.
AI-written summary · about
chapters (11)
- 0:00Type checking intro
- 1:00Hylo language overview
- 3:54Traits and generics
- 6:24Recursive type constraints
- 8:11Undecidable type equality
- 10:17Free monoids explained
- 13:07Undecidability in type systems
- 14:52Rewriting rules for equality
- 20:24Fixing non-confluent systems
- 22:33Universal quantification
- 24:18Summary and future
related talks
01h 03mVerifying Dependent Type-checkers
32mVerifying Haskell's Rewrite Rules based on Polymorphic Rewriting Theory
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
30mConstraint Typing with Boolean Algebra
46mThe Calculated Typer (Functional Pearl)
21mChecking Equivalence in a Non-strict Language
26mType Narrowing the Hard Way
15mRegular Language Type Inference with Term Rewriting