Erasure In Dependently Typed Programming
summary
Presents an erasure-inference pipeline that numbers binders and applications, emits Horn-clause constraints about retention, solves them for a minimal set of runtime values, and substitutes to produce a plain-runtime program. Proves erasure commutes with reduction under confluence and subject reduction. Implements the pipeline for Idris → Chicken Scheme and reports large compile-time and code-generation savings on three benchmarks, plus enabling newtype, identity and nat optimizations. Notes problems: separate compilation, erasure polymorphism and unpredictable inference; recommends explicit annotations or constraint-bearing signatures.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:25Erasure in dependently typed programming
- 8:15Problems with traditional erasure
- 13:57Irrelevance vs runtime erasure in Agda
- 17:34Lazy implicits aren't enough for erasure
- 22:57Phase distinction for erasure
- 34:24Erasure inference in practice
- 41:08Benefits for compiler optimizations
- 43:15Future work in erasure
- 51:08Conclusion
- 52:35Q&A
related talks
14mA dependently typed calculus with pattern matching and erasure inference
31mDependent tagless final
25mBinding Syntax for Dependently-Typed Programs
18mDeferring the Details and Deriving Programs
24mImperative Syntax for Dependent Types
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
22mA Dependent Language with Type-Safe Program Extraction