Dependent tagless final
summary
Proposes a dependent tagless‑final embedding implemented in Idris using quantitative type theory and Elab/TT‑imp metaprogramming to compose three concrete fragments (base: int ops, read: scoped reads, var: named lambdas) while keeping multi‑staging. Finds that lambda abstraction blocks compile‑time reduction for subterms; fixes this by adding a specialized term‑rewriting interpreter plus a delegating interpreter that chooses a narrower or wider context so reductions run at compile time. Implements only the read effect in the paper and reports stubborn limits on reusable expressions and interpreter reuse.
AI-written summary · about
chapters (18)
- 0:00Types
- 1:12Dependent type
- 1:50Quantitative type theory
- 3:40Auto parameters
- 5:09Interfaces
- 6:20Naming interfaces
- 7:41Passing interface parameters
- 8:19Determining interface parameters
- 8:43Meta programming facilities
- 10:36Context
- 11:22Approach
- 13:07Implementation
- 14:50Interpreters
- 16:36Dependent types
- 18:43In practice
- 19:34Summary
- 25:36Limitations
- 26:40Questions
related talks
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
42mFunctional interpreters and you
19mTowards Tagless Interpretation of Stratified System F (Extended Abstract)
01h 07mErasure In Dependently Typed Programming
20mFirst-class Algebraic Presentations with Elaborator Reflection (Extended Abstract)
15mElaboration with First-Class Implicit Function Types
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
24mImperative Syntax for Dependent Types