Binding Types à la carte
Please log in to watch this conference skillscast.
Imagine you want to write a data type for an abstract syntax tree with binders. You get started, write a function for substitution. Get lost in the renaming story.
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:
Thanks to our sponsors
Binding Types à la carte
Arnaud Spiwack
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.
Please log in to watch this conference skillscast.
Imagine you want to write a data type for an abstract syntax tree with binders. You get started, write a function for substitution. Get lost in the renaming story.
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:
Thanks to our sponsors
Binding Types à la carte
Arnaud Spiwack
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.