Binding Syntax for Dependently-Typed Programs
summary
Proposal adds customizable binder syntax to dependently-typed code, implemented in the Idris compiler as a fixed-grammar desugaring that desugars to lambda application and flips arguments so binders on the left supply scope for the right-hand expression. Concrete behavior: nested indexed binders become readable, operator-style binders work, and common mistakes yield targeted diagnostics (e.g., hint to import a module or fix operator definition) instead of vague "not in scope" errors. Feature is implemented and exercised, not merely theoretical.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:47Programming language design pillars
- 8:34Dependent type syntax problem
- 10:00Nested sigma types symmetry
- 11:25Idris and Agda solutions
- 14:13Customizable binder syntax
- 16:21Binder syntax implementation
- 18:50Beyond containers use cases
- 21:18Syntax design in compilers
- 22:43Future directions
- 23:24Q&A
related talks
24mImperative Syntax for Dependent Types
01h 07mBuilding a Dependently Typed Language in Haskell Part 1
01h 07mErasure In Dependently Typed Programming
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
23mFormalizing Monoidal Categories and Actions for Syntax with Binders
19mCombining Dependency, Grades, and Adjoint Logic
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
31mDependent tagless final