Skip to content

General Composition

Archived page

This page is kept for reference and its original URL still works, but it is not part of the current site and is no longer maintained. Dates and links reflect when it was written.

Shown above is a general formulation of composition of operations in dependent type theory, as derived below.

Tuple Functors

If \(n\) is a natural number, we write \(n \colon \mathbb N\) and say "\(n\) has type \(\mathbb N\)." (For the reader unfamiliar with type theory, it's safe in the beginning to think of this as meaning \(n\in \mathbb N\).)

For \(n \colon \mathbb N\), we denote and define \(\underline{n} = \{0, 1, \dots, n-1\}\).

For \(m \colon \mathbb N\), denote and define the \(\mathrm{mtuple}\) functor on Set as follows:

  • on objects: if \(A\) is a Set, then \(\mathrm{mtuple} A = \{(a_{0}, \dots, a_{m-1}) \mid a_{i} \colon A\}\)

  • on arrows: if \(f \colon A \to B\) is a function from the set \(A\) to the set \(B\), then \(\mathrm{mtuple} f \colon \mathrm{mtuple}A \to \mathrm{mtuple}B\) is defined for each \((a_{0}, \dots, a_{m-1})\) of type \(\mathrm{mtuple}A\) as follows: \(\(\mathrm{mtuple}f (a_0, \dots, a_{m-1}) = (f a_0, \dots, f a_{m-1}),\)\) which inhabits the type \(\mathrm{mtuple} A\).

Notice that \(\mathbf a\) has type \(\mathrm{mtuple} A\) iff we can represent \(\mathbf a\) as a function of type \(\underline{m} \to A\); that is, iff we can represent the mtuple \((a_0, \dots, a_{m-1})\) as a function, \(\mathbf a\), where \(\mathbf a(i) = a_i\) for each \(0\leq i < n\). Thus, we have the following equivalence of types: \(\mathrm{mtuple} A \cong \underline{m} \to A\).

Let \(\mathbf m = (m_0, \dots, m_{n-1}) \colon \mathrm{ntuple} \mathbb N\). Define the \(\mathbf{mtuple}\) functor as follows:

  • on objects: if \(A\) is a Set, then \(\(\mathbf{mtuple} A = \{((a_{00}, \dots, a_{0(m_1-1)}), \dots, (a_{(n-1)0}, \dots, a_{(n-1)(m_n-1)})) \mid a_{ij} \colon A\}\)\) (We may write \(\mathbf a_i\) in place of \((a_{i0}, \dots, a_{i(k-1)})\), if \(k\) is clear from context.)

  • on arrows: if \(f\) is a function from the set \(A\) to the set \(B\), then \(\mathbf{mtuple} f \colon \mathbf{mtuple}A \to \mathbf{mtuple}B\) is defined for each \((\mathbf a_1, \dots, \mathbf a_n)\) in \(\mathbf{mtuple}A\) as follows: \begin{align}\mathbf{mtuple} f (\mathbf a_1, \dots, \mathbf a_n) &= (\mathrm{m_1tuple}f \mathbf a_1, \dots, \mathrm{m_ntuple}f \mathbf a_n)\ &= ((f a_{11}, \dots, f a_{1m_1}), \dots, (f a_{n1}, \dots, f a_{nm_n})).\end{align}

Notice that \(\mathbf a_i\) has type \(\mathrm{m_ituple} A\) iff it can be represented as a function of type \(\underline{m_i} \to A\); that is, iff the tuple \((a_{i0}, \dots, a_{i(m_i-1)})\) is (the graph of) the function defined by \(\mathbf a_i(j) = a_{ij}\) for each \(0\leq j < m_i\). Thus, if \(\mathbf m = (m_0, \dots, m_{n-1}) \colon \mathrm{ntuple} \mathbb N\), then \(\mathbf{mtuple} A\) is the dependent function type, \(\(\prod_{i \colon \underline{n}} (\underline{m_i} \to A).\)\)

Fork and Eval

Define \(\mathrm{fork} : (A \to B)\to (A \to C) \to A \to (B \times C)\) as follows: if \(f \colon A \to B\), \(g \colon A \to C\), and \(a \colon A\), then \(\mathrm{fork} (f) (g) (a) = (f (a), g (a))\).

(A more standard definition of fork might take the domain to be \((A \to B)\times (A \to C)\), whereas we have described a "curried" version in order to support partial application.)

The fork function generalizes easily to dependent function types. Let \(A\) be a type and for each \(a \colon A\) let \(B_a\) and \(C_a\) be types. Define the dependent fork, denoted by \(\(\mathbf{fork} : \prod_{a : A} B_a\to \prod_{a : A} C_a \to \prod_{a : A}(B_a \times C_a),\)\) as follows: if \(f \colon \Pi_{a : A} B_a\), \(g \colon \Pi_{a : A} C_a\), and \(a \colon A\), then \(\mathbf{fork} (f) (g) (a) = (f (a), g (a))\colon B_a \times C_a\). Since we use a curried definition, we can partially apply \(\mathbf{fork}\) and obtain the expected typing relations, viz., \(\(\mathbf{fork} (f) \colon \prod_{a:A} C_a \to \prod_{a:A} (B_a \times C_a)\quad \text{ and } \quad \mathbf{fork} (f) (g) \colon \prod_{a:A} (B_a \times C_a).\)\)

Next, let \(\mathbf{eval} \colon (A \to B) \times A\) denote function application; that is, \(\mathbf{eval} (f, a) = f a\), if \(f \colon A \to B\) and \(a \colon A\). Thus, if \(h \colon \prod_{a : A}(C_a \to D)\), \(k \colon \prod_{a : A}C_a\), and \(a\colon A\), then \(\(\mathbf{fork} (h)(k)(a) = (h(a), k(a)) \colon (C_a \to D) \times C_a, \text{ and }\)\) \(\(\mathbf{eval} \circ \mathbf{fork} (h)(k)(a) = h(a)k(a) \colon D.\)\)

General Composition of Operations on a Set

In universal algebra we deal mainly with finitary operations on sets. By an \(n\)-ary operation on the set \(A\) we mean a function \(f \colon A^n \to A\), that takes \(n\) inhabitants of the type \(A\) and returns an element of type \(A\).

By the equivalence of the \(\mathrm{ntuple}\) type and the function type \(\underline{n} \to A\), we may represent the type of \(n\)-ary operations on \(A\) by \((\underline{n} \to A) \to A\). Evaluating such an \(f \colon (\underline{n} \to A) \to A\) at a tuple \(a \colon \underline{n} \to A\) is simply function application, expressed by the usual rule (sometimes called "implication elimination" or "modus ponens").

If we let \(a_i\) denote the value of \(a\) at \(i\), and if we identify \(a\) with it's graph (the tuple \((a_0, \dots, a_{n-1})\)), then \(f a = f(a_0, \dots, a_{n-1})\).

Denote and define the collection of all finitary operations on \(A\) by \(\(\operatorname{Op}A = \bigcup_{n<\omega} (A^n \to A)\cong \bigcup_{n<\omega} ((\underline{n} \to A) \to A).\)\)

We will now try to develop a formulation of general function composition that is more elegant and computationally practical than the standard formulation. Let us first briefly review the standard formulation of function composition. Let \(f \colon (\underline{n} \to A) \to A\) be an \(n\)-ary operation on \(A\), and suppose for each \(0\leq i < n\) we have an operation \(g_i \colon (\underline{k_i} \to A) \to A\). Then we define \(f \circ (g_0, \dots, g_{n-1})\) in the following standard way: for each \(\(((a_{00}, \dots, a_{0(k_0-1)}), \dots, (a_{(n-1)0}, \dots, a_{(n-1)(k_{n-1}-1)}))\colon A^{k_0} \times \cdots \times A^{k_{n-1}},\)\) \begin{align}(f\circ &(g_0, \dots, g_{n-1}))((a_{00}, \dots, a_{0(k_0-1)}), \dots, (a_{(n-1)0}, \dots, a_{(n-1)(k_{n-1}-1)}))\ &= f(g_0(a_{00}, \dots, a_{0(k_0-1)}), \dots, g_{n-1}(a_{(n-1)0}, \dots, a_{(n-1)(k_{n-1}-1)})).\end{align}

Not only is this notation tedious, but also it lends itself poorly to computation. To improve upon it, let us first consider the ntuple \((g_0, \dots, g_{n-1})\). This is an ntuple of operations from \(\operatorname{Op}A\). If we denote by \(g\) the function from \(\underline{n}\) to \(\operatorname{Op}A\) given by \(g i = g_i\) for each \(0\leq i < n\), then \(g\) inhabits the following dependent function type: \(\(\prod_{i : \underline{n}} ((\underline{k_i} \to A) \to A).\)\)

Next, define the function \(a\) as follows: \(a i \colon \underline{k_i} \to A\) for each \(0\leq i < n\) and for each \(j\colon \underline{k_i}\), \(a i j = a_{ij}\). Then the ntuple of arguments in the expression above can be identified with the tuple \(a = (a 0, \dots, a (n-1))\) of functions. Thus \(a\) has dependent function type \(\prod_{i : \underline{n}} (\underline{k_i} \to A)\), and for each \(i\colon \underline{n}\), we have \(a i j = a_{ij}\).

Now, looking back at the section above, where we defined the fork and eval functions, we can see how to perform general composition using dependent types. If \(g \colon \Pi_{i : \underline{n}} ((\underline{k_i} \to A) \to A)\), and \(a \colon \Pi_{i : \underline{n}}(\underline{k_i} \to A)\), then \(\(\mathbf{fork} (g) (a) (i) = (g(i), a(i)) : ((\underline{k_i}\to A) \to A) \times (\underline{k_i}\to A)\)\) and \(\mathbf{eval} (\mathbf{fork} (g) (a) (i)) = g(i) a(i)\) has type \(A\). Observe that the codomain \(A\) does not depend on \(i\), so the types \(\Pi_{i:\underline{n}} A\) and \(\underline{n} \to A\) are equivalent. Therefore, \(\mathbf{eval} \circ \mathbf{fork} (g) (a)\) has type \(\underline{n} \to A\). On the other hand, we have \(\(\mathbf{eval}\circ \mathbf{fork} (g) : \prod_{i : \underline{n}} (\underline{k_i} \to A) \to (\underline{n} \to A).\)\) Thus, if we take an \(n\)-ary operation, \(f\colon (\underline{n} \to A) \to A\), and an \(n\)-tuple of operations, \(g\colon \Pi_{i : \underline{n}} ((\underline{k_i} \to A) \to A)\), then we can define the composition of \(f\) with \(g\) as follows: \(\(f [g] := f \circ (\mathbf{eval}\circ \mathbf{fork}(g)) : \prod_{i : \underline{n}}(\underline{k_i} \to A) \to A.\)\) Indeed, if \(a \colon \Pi_{i : \underline{n}}(\underline{k_i} \to A)\), then \(\mathbf{eval}\circ \mathbf{fork}(g)(a)\) has type \(\underline{n} \to A\), which is the domain type of \(f\); therefore, \(f (\mathbf{eval}\circ \mathbf{fork}(g) (a))\) has type \(A\), as desired.