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:
- Comparing Strict and Lazy (SkillsCast recorded in November 2020)
- Haskell eXchange 2021: Novice Track (Online Conference on 15th November 2021)
- Haskell eXchange 2021: Pro Track (Online Conference on 16th - 17th November 2021)
- Hashing Modulo Alpha Equivalence (SkillsCast recorded in May 2021)
- In The Belly Of The Whale: Tales From Haskell In The Enterprise (SkillsCast recorded in May 2021)
Binding Types à la carte
Arnaud Spiwack spend the first 10 years of his working life in Academia, between Chalmers university in Gothenburg, Sweden, and Ecole Polytechnique, Inria, and Mines ParisTech, in the Paris area. He spent this time researching dependent types, computer-verified proof, and sequent calculus. During his time in Academia, Arnaud got involved in the development of the Coq Proof Assistant, where he, in particular, re-engineered Coq's tactic engine and gave it an abstract interface. After leaving academia, he remained a member of the core development team of the Coq Proof Assistant. He is now a senior architect at Tweag I/O, and is working at making the world better typed.