In our fourth episode, we speak with Stephanie Weirich from the University of Pennsylvania on the Zombie language and Dependent Haskell. Stephanie is a long-time contributor to Haskell, having been involved in the design and implementation of features such as generalized algebraic datatypes, higher-rank polymorphism, type families, and promoted datatypes. She has also been a participant in Trellys, a project with the goal of combining proofs and programming in the same language.
Zombie is a different kind of dependently typed language, eschewing automatic β-reduction in the type checker for an approach based on explicit equality rewriting, which enables new ways of combining proofs and programs, as well as new forms of proof automation. Meanwhile, as languages designed for dependently typed programming come closer to practical applicability, Haskell is also moving towards full dependent types. We discuss the challenges and opportunities available at the cutting edge of Haskell.
Reading:
- Combining Proofs and Programs in a Dependently Typed Language (With technical appendix) by Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich, POPL 2014
- Programming up to Congruence (Extended version) by Vilhelm Sjöberg and Stephanie Weirich, POPL 2015
- Dependently Typed Programming with Singletons by Richard A. Eisenberg and Stephanie Weirich, Haskell Symposium 2012
- Down with Kinds: Adding Dependent Heterogeneous Equality to FC (Extended Version) by Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg (ICFP 2013)
Video:
- Video lectures on designing dependently typed languages from Oregon Programming Languages Summer School
- Depending on Types — keynote talk on dependent Haskell at ICFP 2014
Code:
- The Trellys repository on Github contains the source code to Zombie
- Pi-Forall, a tutorial implementation of a type checker for a dependently typed language
- Download:
- AAC29 MB
- MP336 MB
- FLAC144 MB
- Opus Audio34 MB