Normalizable types
summary
Proposes an adjusted normalized-quotient design that separates typechecking and runtime reduction so canonicalization runs only during checking and is erased for execution, proving an erasure theorem and a trivial encoding back to the core calculus. Adds a Qcan constructor and requires a computable canonicalizer, keeps definitional equality and strong dependent elimination without new axioms, and preserves decidable typechecking; practical tradeoff: works only when a cheap or computable normalization function exists.
AI-written summary · about
chapters (8)
- 0:00Normalizable types
- 2:28Quotient types in type theory
- 6:17Traditional quotient type challenges
- 8:45Normalized types alternative
- 13:07Double canonicalization with Qcan
- 14:30Type checking vs runtime semantics
- 16:37Efficiency trade-offs
- 16:57Q&A: Normalization limits
related talks
30mNormalisation for First-Class Universe Levels
01h 03mVerifying Dependent Type-checkers
16mThe Normalization Barrier Revisited
14mA dependently typed calculus with pattern matching and erasure inference
36mMcTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory
29mType Checking with Rewriting Rules
23mImpredicative Observational Equality
26mAlgorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach