CoRecursive: Coding Stories Tech Talk: Dependent Types in Haskell with Stephanie Weirich
Jun 13, 2018
In this discussion, Stephanie Weirich, a Professor at the University of Pennsylvania and an expert in dependent types, shares her insights on extending Haskell's type system. She illustrates how dependent types make type checking more powerful, allowing for compile-time validation of elements in heterogeneous dictionaries. Stephanie explains the applications of dependent types in creating safer programs, including parsing expressions. The conversation also touches on the experimental nature of Haskell and the evolution of its language features, offering a glimpse into future possibilities.
AI Snips
Chapters
Transcript
Episode notes
Regex Example with Dependent Types
- Stephanie Weirich shared a regex example using dependent types capturing group names and presence at compile time.
- The type system guarantees keys exist and encodes multiplicity and optionality of captured groups.
Safe Heterogeneous Dictionaries
- Dependent types enable compile-time checked heterogeneous dictionaries derived from regex capture groups.
- Accessing a missing capture group key causes a compile-time error, eliminating runtime mistakes common in dynamic languages.
Index Types Link Types and Values
- Index types let data structures be precisely constrained by compile-time values, linking type and runtime data.
- This enables expressing exact dictionary shapes keyed by strings with associated types known at compile time.