Richard Eisenberg on Dependent 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.
www.meetup.com/NY-Haskell/eve...

[@sevenhong5809]

0:52 - 6:09 all these type related features are actually equally interesting as the topic of this video

[@asitisj]

30:50 when you encode length of the list as the type, are you carrying induction over the initial list

[@TheDickswab]

Great video, though there's a lot of material teased that he unfortunately didn't manage to get through!

[@alexanderskladovski]

Such a shame they didn't give him enough time...

[@noninvasive_rectal_probe8990]

Absolutely useless