Richard Eisenberg on Dependent Types

Richard Eisenberg presents Stitch, a typed lambda-calculus interpreter written in Haskell using type-indexed abstract syntax and advanced types.

Stitch: The Sound Type-Indexed Type Checker Richard Eisenberg will present his work on Stitch, a typed lambda-calculus interpreter, written in Haskell using type-indexed abstract syntax. The datatype that represents expressions in the interpreter is indexed by its Stitch type, meaning that only well-typed expressions can be represented. However, Stitch is not just a toy example: the interpreter is an application with a REPL, and thus contains a parser and type-checker. It also can optimize expressions via a common-subexpression-elimination pass and presents a flexible, expressive user interface that can be used to teach the lambda-calculus. The implementation of Stitch taps into a wide range of Haskell features for working with fancy types, including generalized algebraic datatypes (GADTs), existentials, higher-rank types, singletons, and the new type-indexed TypeRep feature. This talk will include a brief introduction to these features and use Stitch as a case study to show that Haskell is ready to support fancy types used in anger, even though it still lacks support for full dependent types. Richard is an Assistant Professor of Computer Science at Bryn Mawr College, an undergraduate-focused women's college in suburban Philadelphia. He is a 2016 graduate from the PhD program at the University of Pennsylvania, where he worked with Stephanie Weirich. His dissertation was on a design for the surface syntax, internal language, and type inference algorithm to support dependent types in GHC; he is a core contributor to GHC and is currently funded by an NSF grant to implement dependent types in GHC. meetup.com/NY-Haskell/events/249575016/