Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Fri 28 Aug 2020 15:30 - 16:00 at Haskell - Paper Session 5 - Types Chair(s): Jurriaan Hage

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)49KiB

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 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

14:30 - 16:00: Paper Session 5 - TypesHaskell at Haskell
Chair(s): Jurriaan HageUtrecht University, Netherlands
14:30 - 15:00
Staged Sums of Products
Matthew PickeringUniversity of Bristol, UK, Andres LöhWell-Typed LLP, Nicolas WuImperial College London, UK
15:00 - 15:30
Eliminating Bugs with Dependent Haskell (Experience Report)
Noam ZilbersteinFacebook, USA
15:30 - 16:00
Stitch: The Sound Type-Indexed Type Checker (Functional Pearl)
DOI File Attached