Before we continue on, it is worth pausing for a moment to consider what a fold does: given appropriate parameters (values or functions), it works by cases to de-construct a value of some structured type (e.g. a list or tree), systematically transforming the pieces of the structure (the arguments of the constructor for each case) into some common result type. Of course, the parameters themselves will need to have types appropriate for this conversion to be well-defined:
[], we need just a
value of the result type to return in its place;
Lit, which takes a single
argument, we will need a function mapping an argument of that type to a
result of the new result type;
: or Bop,
which take several arguments, some of which are recursive structures,
we will need a function mapping arguments of the several types to a
result of the new result type, but now the arguments corresponding to
recursive instances of the type will actually be of the result type, since
the fold will have been applied recursively in those positions.
We will be using folds for various types a lot in the remainder of the course, so it will behoove you to try and get a handle on what they are, how they work and how they are defined for each new type. From a languages perspective, each new data type represents a language, and the fold for that data type represents a kind of general semantic function for the language, waiting to be applied to (or instantiated with) specific semantic components for the structurally smaller sub-languages from which it is built. Another way to think of the folds is as a kind of canonical generic converter/transformer/eliminator which, when suitably instantiated, resolves or eliminates that structure in favor of some new result, systematically consuming the given type at all recursive occurrences.
fold to be defined once and for all, for
any type: the trick is to think of types themselves as a kind of structured
value and work by cases on the structure of types (alternatives or sums,
products, parameters, recursions, ...)