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

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.

• What are you trying to accomplish here? For instance, why not just take ordered pairs as primitive, as is standard in STLC? Also, are thes sets that you wrote down, e.g., $\{a, g, b\}$ supposed to be terms of the $\lambda$-calculus? What are their types? How is union incorporated into STLC? – Andrej Bauer Aug 15 at 19:32
• @Andrej Bauer Yes, I could do this by having a function $\lambda z'_{\beta \times \alpha}, z. \,(z,\, \pi_1 z',\, \pi_2 z')$ (where $\pi_1, \pi_2$ are projection functions) applied to the ordered pair $(g, b)$, and then applying this to $a$. But, in the context of a natural language semantic theory, stuffing it full of functions such as these is highly undesirable. It would be more desirable for me to have an operation like the unit of a monad, which lifts $a$ into $(a)$, and then combines this with other tuples to form larger tuples. I am looking for that. I don't know whether it exists. – user65526 Aug 15 at 20:45
• @Andrej Bauer, yes, correct, and they are supposed to be lambda terms of different types. Section 2.1 of this arxiv.org/pdf/cs/0205026.pdf discusses the powerset monad in a natural language semantics context. I realise now that maybe this can't work as suggested, since we are unioning things of different types. – user65526 Aug 15 at 20:48
• Before I try to answer, may I ask what your research background is? Your question is stated in a confusing way, so I am trying to callibrate my answer. – Andrej Bauer Aug 15 at 21:10
• If the answer "You are looking for the list monad]" is sufficiently comprehensible, then we might be done. But I am extrapolating quite a bit from what you wrote and trying to guess what the actual question is. – Andrej Bauer Aug 15 at 21:12

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$$.

• thanks. Yes, I am coming from outside of your community. The list monad would be absolutely perfect, except I need to form lists of things of different type, such as $[John:e, sleep: e \to t ]$. That's why I've been considering the alternative route of using tuples, and creating larger and larger tuples successively, via lambda terms such as the one I wrote in my comment above($\lambda z'_{\beta \times \alpha}, z. \,(z,\, \pi_1 z',\, \pi_2 z')$). If there was something like the list monad, but for tuples, that would be great, or a special concept of list which allows lists of different types. – user65526 Aug 15 at 21:35
• It is a common misconception that heterogenous lists are a good idea. It is far more likely that you really want to form a sum type $S$ of all the possible types that could appear in the list, and use a list of $S$'s. If you really need heterogenous lists, you will have to make your life complicated by passing to dependent types or some such. – Andrej Bauer Aug 15 at 21:54
• I think the original sin here is that you're introducing constants of arbitrary types. That feels like the wrong level to me. – Andrej Bauer Aug 15 at 21:55
• Ah, so we have,to give one example $e \to t + e$, as a sum type,and then we construct a list of things of type $e$ and type $e \to t$.The problem with that is that I need to be able to have arbitrary types in the list, because there could be at least 30 types that would need to be put into the sum type!Words in natural language are represented with lambda terms and there are many words.So we would end up with a crazy number of types to consider.If we could have a union type which was recursive maybe that would work. – user65526 Aug 15 at 22:02
• Alternatively, maybe having primitive tuples is the way to go. But then I would clutter up my derivations of the meanings of sentences with functions which I do not want to have. – user65526 Aug 15 at 22:03