Monoid Comprehesion

The concept of monoid homomorphism is useful for expressing a formal semantics of iteration over collections. However, it is not very convenient as a programming construct. A natural notation for such a construct that is both conspicuous and can be expressed in terms of monoid homomorphisms is a monoid comprehension. This notion generalizes the familiar notation used for writing a set in comprehension (as opposed to writing it in extension) using a pattern and a formula describing its elements (as oppposed to listing all its elements). For example, the set comprehension $\{\pr(x,x^2)\;\vert\;x\in\NN , \exists n.x=2n\}$ describes the set of pairs $\pr(x,x^2)$ (the pattern), verifying the formula $x\in\NN , \exists n.x=2n$ (the qualifier).

This notation can be extended to any (primitive or collection) monoid $\oplus$. The syntax of a monoid comprehension is an expression of the form &oplus#oplus;{e[]Q} where $e$ is an expression called the head of the comprehension, and $Q$ is called its qualifier and is a sequence $q_1,\ldots,q_n$, $n\geq0$, where each $q_i$ is either

• a generator of the form $x\from e$, where $x$ is a variable and $e$ is an expression; or,

• a filter $\phi$ which is a boolean condition.

In a monoid comprehension expression &oplus#oplus;{e[]Q}, the monoid operation $\oplus$ is called the accumulator.

As for semantics, the meaning of a monoid comprehension is defined in terms of monoid homomorphisms.

DEFINITION 3.28.1 (Monoid Comprehension)   The meaning of a monoid comprehension over a monoid $\oplus$ is defined inductively as follows:

$$\renewedcommand{arraystretch}{1.6}\begin{array}{l@{\;\eqd \;}... ...c, Q} & \ite {c}{\comp {\oplus}{e}{Q}}{\Z {\oplus}} \end{array}$$

such that $e:\Ty {\oplus}$, $e':\Ty {\odot}$, and $\odot$ is a collection monoid.

Note that although the input monoid $\oplus$ is explicit, each generator $x\from e'$ in the qualifier has an implicit collection monoid $\odot$ whose characteristics can be inferred with polymorphic typing rules.

Although Definition 3.28.1 can be effectively computed using nested loops (i.e., using the iteration semantics (3.13)), such would be in general rather inefficient. Rather, an optimized implementation can be achieved by various syntactic transformation expressed as rewrite rules. Thus, the principal benefit of using monoid comprehensions is to formulate efficient optimizations on a simple and uniform general syntax of expressions irrespective of specific monoids.

Thus, monoid comprehensions allow the formulation of ``declarative iteration.'' Note the fact mentioned earlier that a homomorphism coming from the translation of a comprehension encapsulates the operation in its function. Thus, this is generally taken to advantage with operations that cause a side-effect on their second argument to enable an in-place homomorphism to dispense with unneeded intermediate computation.