A Dependently Typed Language with Dynamic Equality

Explore a 19-minute conference talk from TyDe 2023 that introduces a novel dependently typed language with dynamic equality. Discover how this approach addresses usability issues in dependent type systems by delaying equality checking until runtime, potentially transforming static errors into warnings. Learn about the language's blame system for clear error messaging, its handling of dependent indexed data and pattern matching, and the correctness properties proven for a fragment of the language. Gain insights into the potential benefits of this system for functional programmers and its implications for bug prevention in software development.

Introduction
Why type checking
Surface language
Cast language
elaboration
Questions
Handling Data
Unification