Lambda the Ultimate

Functor is to Lens as Applicative is to Biplate: Introducing Multiplate is an interesting paper by Russell O'Connor which shows that certain types are isomorphic to quantification over certain type classes. This isomorphism then naturally leads to a generalization of Uniplate/Compos into Multiplate, which allows for rather generic traversals.

The BiplateType datatype defined in the Uniplate library is similar to a lens (a.k.a. a functional reference). This paper proves that Biplate generalizes lens similarly to how applicative functor generalizes functor. This paper gives an alternative definition of BiplateType using a nested data type that better captures the invariants for Biplates than Uniplate's original definition. In previous work, van Laarhoven conjectures an isomorphism between this nested data type and a data type found in Compos library. This paper complete his proof of the isomorphism by using free theorems for types polymorphic over applicative functors. This result means that, morally speaking, Compos and Uniplate use isomorphic representations for their core data type for generic traversals of simple recursive data types. For mutually recursive data types, Compos and Uniplate providing two different extensions to this common core functionality. Compos requires the user to rewrite a mutually recursive data type as a GADT, while Uniplate's Biplate class, is less powerful but only requires multiparameter type classes and does not require rewriting one's data type. This paper proposes a third extension to support mutually recursive datatypes that is as powerful as Compos, as easy to use as Biplate, and more portable than both of them. This proposal, called Multiplate, only requires rank 3 polymorphism.

(Full disclosure: Russell is a post-doc at McMaster, working with me and Bill Farmer. While trying to figure out how to make certain repetitive traversals of MathScheme ASTs into a generic framework, he 'stumbled upon' multiplate, and then kept pursuing the ideas, with the multiplate package and this nice bit of theory as the end result.)