Arnaud Spiwack

Arnaud Spiwack spent 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 a better typed place.

The Haskell base library features the Data and Control module hierarchies. The distinction between data and control is rooted deeply, in computer science: it can already be seen in Turing machines. However, when it comes to Haskell the difference between data and control can be quite muddled. A case in point is functors: there are functor type classes in both hierarchies: Functor and Traversable are in the Data hierarchy, while Applicative and Monad are in the Control hierarchy. This is really confusing! Do functors magically cease to be data and become control structure when I declare a Applicative instance?

In this talk, I will show that there are indeed two kinds of functors, which I dub data functors, and control functors. Each fitting in the respective hierarchy. The catch is that you can’t tell them apart in regular Haskell. However, with the new linear types extension, we can see them for what they really are. In fact, when programming with linear types, one typically needs both kinds. I’ll be explaining a tiny bit of linear types, just enough to expose the two hierarchies for what they are.