A Dependently Typed Language with Dynamic Equality
summary
Designs a dependently typed language that defers equality checking to runtime and replaces many static rejections with warnings, inserting explicit casts and assertions during elaboration so failing equalities raise runtime errors with precise blame. Implements bidirectional elaboration to a cast language, records unification steps for pattern matching on indexed data, proves cast soundness for a fragment (without full data formalization), and ships a working prototype.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:58Why type checking
- 3:03Surface language
- 3:39Cast language
- 7:52elaboration
- 8:58Questions
- 12:52Handling Data
- 13:57Unification
related talks
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
18mDeveloping a Dependently Typed Language with Runtime Proof Search
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
01h 07mBuilding a Dependently Typed Language in Haskell Part 1
15mTaming Type Annotations in Gradual Typing
19mIll-Typed Programs Don't Evaluate
27mDecomposable Type Highlighting for Bidirectional Type and Cast Systems
25mRobust Dynamic Embedding for Gradual Typing