Gradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
summary
A dependently typed surface language elaborates into a runtime cast language that defers equality checks until execution, runs programs that static checking would reject, and only fails when it finds a concrete witness of constructor inequality. The implementation on GitHub proves cast soundness and gradual-guarantee-like properties, adds a separate blame judgment to extract precise runtime equality errors, and models casts under application so eliminators don’t block. It is a programmer-first, logically unsound prototype that needs more type annotations and better dependent pattern matching for data.
AI-written summary · about
chapters (7)
- 0:00Start
- 5:26Limitations of the System
- 8:42The Dependent Type Theory
- 14:14Elaboration Procedure
- 15:13Rules for the Elaboration Procedure
- 16:47Dependent Eliminators
- 17:20Automated Testing
related talks
19mA Dependently Typed Language with Dynamic Equality
18mDeveloping a Dependently Typed Language with Runtime Proof Search
15mTaming Type Annotations in Gradual Typing
27mDecomposable Type Highlighting for Bidirectional Type and Cast Systems
27mTaming Unsoundness with Gradual Abstract Interpretation
19mIll-Typed Programs Don't Evaluate
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
01h 07mBuilding a Dependently Typed Language in Haskell Part 1