A dependently typed calculus with pattern matching and erasure inference
summary
A dependently typed calculus with pattern matching and explicit erasure annotations is presented, with the central claim that erasure commutes with reduction (and preserves convertibility assuming Church–Rosser). An erasure inference algorithm for unannotated or partial programs is implemented and proved sound, complete and optimal relative to the typing rules. A prototype compiler erases large implicit arguments, recovers intended asymptotic runtime, and shortens end-to-end compilation times in published benchmarks.
AI-written summary · about
chapters (4)
related talks
01h 07mErasure In Dependently Typed Programming
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
22mA Dependent Language with Type-Safe Program Extraction
19mIll-Typed Programs Don't Evaluate
16mAn Intrinsically Typed Compiler for Algebraic Effect Handlers
15mLiberating Merges via Apartness and Guarded Subtyping
13mA Simpler Encoding of Indexed Types
46mThe Calculated Typer (Functional Pearl)