Stitch: The Sound Type-Indexed Type Checker (Functional Pearl)

This talk presents Stitch, a type-indexed interpreter in Haskell that leverages GADTs and type indices to build a sound type checker.

icfp20.sigplan.org/details/haskellsymp-2020-papers/3/Stitch-… 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.