Functors

Each data or type definition introduces a new `map' function (or functor, for category theorists) with the same name and arity as the type constructor. For example, the type definition

      data tree alpha == Empty ++ Node (tree alpha) alpha (tree alpha);
also defines a function
      tree : (alpha -> beta) -> tree alpha -> tree beta
that maps a function over trees. This automatic definition may be explicitly overridden.

It's a little more complicated: if the type argument is used negatively, as in

      type cond alpha == alpha -> bool;
the function will have a flipped type:
      cond : (alpha -> beta) -> tree beta -> tree alpha
If the argument is used both positively and negatively, as in
      type endo alpha == alpha -> alpha;
the function will have a type like
      endo : (alpha -> alpha) -> tree alpha -> tree alpha
Similarly, an abstype definition declares this corresponding function. In order to determine the type, each argument is assumed to be used both positively and negatively unless the argument variable is replaced with one of the special keywords pos, neg or none (indicating that the argument is unused). See the previous appendix for some examples.



Ross Paterson <ross@soi.city.ac.uk>