SkillsCast

Binding Types à la carte

haskell quantified-constraints category-theory algebraic-data-types binders abstract-syntax-trees

11th October 2018 in London

There are 38 other SkillsCasts available from Haskell eXchange 2018

Please log in to watch this conference skillscast.

Ok. You've heard about this de Bruijn index stuff. You get started. But you get lost again in the shifts and the lifts. Wouldn't it be nice if types could help you get all of this binder story right? After all, you're writing Haskell.

Arnaud will present a way to do just that: it's like de Bruijn indices, but with types. It also makes it possible to extend types-with-binders piecewise in the same style as the data type à la carte. Interestingly α-equivalent terms are equal in this representation, which is nice if you want to store the terms in tables, or use memoisation. And it all uses algebra! After all, you're writing Haskell. This story involves functors of functors (not a typo), higher catamorphisms, and Generic1 instances (not a typo either), as well as a brand new feature from GHC 8.6: quantified constraint.

YOU MAY ALSO LIKE:

Thank you to our sponsors and partners

Platinum

Silver

Partners

About the Speaker