Imperative Syntax for Dependent Types
summary
Claim: an imperative surface syntax that elaborates into Idris makes dependently typed code more comprehensible for experienced imperative programmers. Built: a read-only prototype plus transformation algorithms that turn loops, block statements, pattern matching and reassignment into Idris terms, and an algorithm that derives decidable equality for user types automatically. Works: elaboration succeeds for well-typed programs but error reporting and totality/termination checks remain unresolved. Next step: a formal user study to measure readability and usability across imperative-language backgrounds.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 6:08ADTs and pattern matching
- 8:41Hypothesis on imperative syntax
- 10:48Designing Idris layer
- 13:38Basic syntax
- 15:30Block statements and reassignment
- 16:35Adding loops
- 17:38Dependent types without proofs
- 19:04Decidable equality
- 19:47Putting it all together
- 20:28Q&A
related talks
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
39mDependent Type Driven Program Synthesis in Idris
43mIdris 2: Type-driven development of Idris
25mBinding Syntax for Dependently-Typed Programs
12mIdris2-Table: Evaluating dependently-typed tables with... (Extended Abstract)
19mIll-Typed Programs Don't Evaluate
31mDependent tagless final
20mFirst-class Algebraic Presentations with Elaborator Reflection (Extended Abstract)