Forming ordered pairs using monads and doing without the Kuratowski encoding of ordered pairs

Question

Suppose we have a set $S$ of constants of the Simply-Typed Lambda Calculus (STLC) various types, and the operation of union $\cup$ which takes two constants and forms their union.

For example, $S$ could be $\{\, a_e, b_e, f_{e \to t}, g_{e \to e \to t}\}$, where $e$ and $t$ are ground types of the STLC and $e \to t$ is a function type. We can then form $\{a, g, b \}$, by unioning $a$, $g$ and $b$. We could do this iteratively, first unioning $g$ and $b$, and thence $a$.

However, suppose we wanted to do this sort of iterative process in the STLC with ordered pairs, forming $(g, b)$ and then $(a, g, b)$. One way might be to use the Kuratowski encoding of ordered pairs, and use union as before, as well as a singleton-forming operation $\zeta$. We would therefore add to the STLC $\zeta$ and $\cup$. In the Kuratowski encoding, $(a, g, b)$ is defined as $(a, (g, b))$, which in turn is defined as $\{ \{a \}, \{ \{g \}, \{g, b \} \} \}$.

Take $\{ \{g \}, \{g, b \} \}$. We could form this by applying $\zeta$ to $g$ and $\zeta$ to $b$ and then unioning $\{g\}$ and $\{b \}$ to form $\{g, b \}$, applying $\zeta$ to the result to form $\{ \{g,b \} \}$ and then applying $\zeta$ twice to $g$, and unioning $\{ \{ g \}\}$ and $\{ \{g,b \} \}$, to form $\{ \{g \}, \{g, b \} \}$. Then a function of the following kind could be written:

$$\lambda b, a. \zeta \, \zeta \,\zeta\, a \,\cup \,\zeta\,(\zeta\,\zeta\, g \cup \zeta\,(\zeta \,g\cup \zeta\,b)))$$

Another way would be to use the powerset monad, where

• the unit $\eta$ of the monad takes an element and forms a singleton
• the join of the monad $\mu_A : \mathcal{P}(\mathcal{P}(A)) \to \mathcal{P}(A)$ is union, i.e., $\mu_A(S) = \bigcup_{B \in S} B$.

For $M \in \mathcal{P}(A)$ and $K : A \to \mathcal{P}(B)$ we have $$M \star K = \bigcup_{x \in M} K(x) = \mu_A(\{K(x) \mid x \in M\})$$

We can compute the union of two subsets $X, Y \subseteq S$ as \begin{multline*} \{\mathbf{false}, \mathbf{true}\} \star (\lambda b : \mathbf{bool} \,.\, \mathbf{if}\,b\,\mathbf{then}\,X\,\mathbf{else}\,Y) \\ = \bigcup \{\mathbf{if}\,b\,\mathbf{then}\,X\,\mathbf{else}\,Y \mid b \in \{\mathbf{false}, \mathbf{true}\} \} = \bigcup \{X, Y\} = X \cup Y. \end{multline*}

We could then form (a, g, b), by applying the $\bigstar$ iteratively, to create the Kuratowski encoding of $(a, g, b)$.

However, both these constructions have to go through the laborious detour of forming a set which, by the Kuratowski encoding, constitutes an ordered pair.

I am looking for a monad or applicative which allows us to form tuples such as $(a, g, b )$ in a more direct way than the ways just described, or simply in an alternative way.

Answer 1

I am not sure I understand your question, but my best guess is that you are looking for the list monad. I am also guessing from the comments you made that you are coming from outside of our community.

There is a difference between tuples and lists. You want lists, and they form a monad.

Given any type $A$, let $L(A)$ be the type of finite lists of elements from $A$. That is, the elements of $L(A)$ are finite sequences $[x_1, \ldots, x_n]$ where $x_1, \ldots, x_n \in A$. The functorial action of $L$ takes $f : A \to B$ to the map $L(f) : L(A) \to L(B)$ which is defined by $L(f)[x_1, \ldots, x_n] = [f(x_1), \ldots, f(x_n)]$.

The monad structure is as follows:

• the unit $\eta_A : A \to L(A)$ is defined by $\eta_A(x) = [x]$.
• the monad multiplication $\mu_A : L(L(A)) \to L(A)$ is concatenation of lists, $$\mu_A [[x_{1,1}, \ldots, x_{1,n_1}], \ldots, [x_{m,1}, \ldots, x_{m,n_m}]] = [x_{1,1}, \ldots, x_{1,n_1}, \ldots, x_{m,1}, \ldots, x_{m,n_m}].$$

All of this can be easily defined formally using algebraic types, see for instance the Haskell definition.

Supplemental:

If you really want heterogenous lists, you need to pass to a more complicated type theory. Let $U$ be the universe, i.e., a type whose elements are types. The dependent sum $\Sigma (A : U) A$ has as its elements pairs $(A, a)$ where $A : U$ and $a : A$. A heterogenous list is then $L(\Sigma (A : U) A)$, which amounts to a finite sequence $[(A_1, a_1), \ldots, (A_n, a_n)]$ where each $A_i$ is a type and $a_i : A_i$.