Showing how some simple mathematical theories naturally give rise to some common data-structures.
Attempting to answer the following questions:
-
Why do lists pop-up more frequently to the average programmer than, say, their duals: bags?
-
More simply, why do unit and empty types occur so naturally? What about enumerations/sums and records/products?
-
Why is it that dependent sums and products do not pop-up expicitly to the average programmer? They arise naturally all the time as tuples and as classes.
-
How do we get the usual toolbox of functions and helpful combinators for a particular data type? Are they ``built into'' the type?
-
Is it that the average programmer works in the category of classical Sets, with functions and propositional equality? Does this result in some ``free constructions'' not easily made computable since mathematicians usually work in the category of Setoids but tend to quotient to arrive in `Sets` —where quotienting is not computably feasible, in `Sets` at-least; and why is that?
And lots of other stuff.