by Peter on December 9, 2005.
Tagged as: Lunches.
I gave a quick guide to a Containers view of parametrised datatypes. With the aid of a couple of examples I introduced the notion of shapes (Nat for lists as the shape of a list is simply it’s length) and positions (indicies where data can be stashed, for lists this is the finite sets Fin). I showed how containers are closed uder Disjoint Union and Cartesian Product, and Least Fix-point if we have W-Types (thus illustrating that the shape of a tree container is a tree with no data in it). I also introduced container morphisms and mentioned that they correspond exactly to natural transformations or polymorphic programs in Haskell.
Thinking about datatypes in this way gives us a number of benefits, for instance some calculations on Data-Types, such as the derivative, fit very nicely into the framework of containers. It is partly for this reason that we are thinking of using an extension to the containers in the above (sorted containers) as datatypes in Epigram2.