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.
www.meetup.com/NY-Haskell/eve...
30 июн 2024
