Stitch: The Sound Type-Indexed Type Checker (Functional Pearl)
A classic example of the power of generalized algebraic datatypes (GADTs) to verify a delicate implementation is the type-indexed expression AST. This functional pearl refreshes this example, casting it in modern Haskell using many of GHC’s bells and whistles. The Stitch interpreter is a full executable interpreter, with a parser, type checker, common-subexpression elimination, and a REPL. Making heavy use of GADTs and type indices, the Stitch implementation is clean Haskell code and serves as an existence proof that Haskell’s type system is advanced enough for the use of fancy types in a practical setting. The paper focuses on guiding the reader through these advanced topics, enabling them to adopt the techniques demonstrated here.
|Stitch tarball (stitch.tar.gz)
Principal Researcher at Tweag I/O. I believe that clever application of theory can eliminate a great deal of programmer errors – specifically, I think fancy types and functional programming are the future. I completed my PhD in 2016 at University of Pennsylvania working under Stephanie Weirich; my dissertation topic was the integration of dependent types into the Haskell programming language. I am a core contributor to the Glasgow Haskell Compiler (GHC).
Fri 28 AugDisplayed time zone: Eastern Time (US & Canada) change
14:30 - 16:00
|Staged Sums of Products
Matthew Pickering University of Bristol, UK, Andres Löh Well-Typed LLP, Nicolas Wu Imperial College London, UKDOI
|Eliminating Bugs with Dependent Haskell (Experience Report)
Noam Zilberstein Facebook, USADOI
|Stitch: The Sound Type-Indexed Type Checker (Functional Pearl)
Richard A. Eisenberg Tweag I/ODOI File Attached