Functors

Modern programming languages employ a variety of data structures which are (at least) sets of “structured elements” equipped with functions that allow combining, manipulating, and querying of such elements. A very rich supply of data types may be built—either directly or recursively—from finite sets using finite products and coproducts. Thus, if A is a character alphabet, A x A x A is “length 3 character arrays.” If pr_f: A x A x A → A is the ith projection, pr _i (w) evaluates the ith coordinate of w, providing the semantics of what would be written as w[i] in many programming languages. A precise definition of length 3 character arrays should specify exactly which maps such as the pr _i should belong to the structure. For a recursive example, define “natural number” by 0 is a natural number if n is a natural number n0 is a natural number which is captured by the recursive specification$${\text{N:: = }}\left\{ 0 \right\} + {\text{N}} \times \left\{ 0 \right\},$$ where we represent each number n by a string of zeros of length n + 1. A central concern will be to provide precise semantics to such specifications.