modular datatypes

Last episode we discussed how functors can describe a single level of a datatype.  In this episode, we discuss how to put these functors back together into a datatype, using disjoint unions of functors and a fixed-point datatype.  The latter expresses the idea that inductive data is built in any finite number of layers, where each layer is described by the functor for the datatype.

This episode continues the discussion of Swierstra's paper "Datatypes à la Carte", explaining how we can decompose a datatype into the application of a fixed-point type constructor and then a functor.  The functor itself can be assembled from other functors for pieces of the datatype.  This makes modular datatypes possible.

In a really wonderful paper of some few years back, Swierstra introduced the idea of modular datatypes using ideas from universal algebra.  Modular datatypes allow one to assemble a bigger datatype from component datatypes, and combine functions written on the component datatypes in a modular way.   In this episode I introduce the paper and the problem (dubbed the expression problem by Phil Wadler) it is trying to solve.  Modular datatypes are a different form of modularity that I would like to consider in the context of the discussion of module systems we have been engaged in now for a while in Chapter 13 of the podcast.