A Dependently Typed Language with Dynamic Equality
Dependent type systems are powerful tools for preventing bugs in programs.
Unlike other formal methods, dependent type systems can reuse the methodology and syntax familiar to functional programmers to construct formal proofs.
However, usability issues, like confusing error messages, often arise from the conservative equalities required by such type theories.
We address this issue by designing a dependently typed language where equality checking is delayed until runtime.
What were once static errors can now be presented to programmers as warnings.
When runtime failures occur, the blame system provides clear error messages indicating the exact static assumption violated during execution.
We present several examples in this system, introduce novel correctness properties, and prove them for a fragment of the language.
Our full system handles dependent indexed data and pattern matching, which are difficult for dependent gradual typing systems to manage.
Finally, we have implemented a prototype of the language.
Mon 4 SepDisplayed time zone: Pacific Time (US & Canada) change
11:00 - 12:30 | TyDe: Type-Driven TypesTyDe at St Helens Chair(s): Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Japan | ||
11:00 22mTalk | A Calculus of Inductive Linear Constructions TyDe DOI | ||
11:22 22mTalk | A Dependently Typed Language with Dynamic Equality TyDe Mark Lemay Autodesk, Qiancheng Fu Boston University, William Blair Boston University, Cheng Zhang Boston University, Hongwei Xi Boston University DOI | ||
11:45 22mTalk | Combining Dependency, Grades, and Adjoint Logic TyDe DOI | ||
12:07 22mTalk | Infix-Extensible Record Types for Tabular DataRecorded TyDe DOI |