<p>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.</p>
<p>There is a difference between tuples and lists. You want lists, and they form a monad.</p>
<p>Given any type <span class="math-container">$A$</span>, let <span class="math-container">$L(A)$</span> be the type of finite lists of elements from <span class="math-container">$A$</span>. That is, the elements of <span class="math-container">$L(A)$</span> are finite sequences <span class="math-container">$[x_1, \ldots, x_n]$</span> where <span class="math-container">$x_1, \ldots, x_n \in A$</span>. The functorial action of <span class="math-container">$L$</span> takes <span class="math-container">$f : A \to B$</span> to the map <span class="math-container">$L(f) : L(A) \to L(B)$</span> which is defined by <span class="math-container">$L(f)[x_1, \ldots, x_n] = [f(x_1), \ldots, f(x_n)]$</span>.</p>
<p>The monad structure is as follows:</p>
<ul>
<li>the unit <span class="math-container">$\eta_A : A \to L(A)$</span> is defined by <span class="math-container">$\eta_A(x) = [x]$</span>.</li>
<li>the monad multiplication <span class="math-container">$\mu_A : L(L(A)) \to L(A)$</span> is concatenation of lists, <span class="math-container">$$\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}].$$</span></li>
</ul>
<p>All of this can be easily defined formally using algebraic types, see for instance the <a href="http://hackage.haskell.org/package/base-4.12.0.0/docs/src/GHC.Base.html#line-984" rel="nofollow noreferrer">Haskell definition</a>.</p>
<p><strong>Supplemental:</strong></p>
<p>If you really want heterogenous lists, you need to pass to a more complicated type theory. Let <span class="math-container">$U$</span> be the universe, i.e., a type whose elements are types. The <a href="https://en.wikipedia.org/wiki/Dependent_type#%7F%27%22%60UNIQ--postMath-00000012-QINU%60%22%27%7F_type" rel="nofollow noreferrer">dependent sum</a> <span class="math-container">$\Sigma (A : U) A$</span> has as its elements pairs <span class="math-container">$(A, a)$</span> where <span class="math-container">$A : U$</span> and <span class="math-container">$a : A$</span>. A heterogenous list is then <span class="math-container">$L(\Sigma (A : U) A)$</span>, which amounts to a finite sequence <span class="math-container">$[(A_1, a_1), \ldots, (A_n, a_n)]$</span> where each <span class="math-container">$A_i$</span> is a type and <span class="math-container">$a_i : A_i$</span>.</p>

CC BY-SA 4.0
2020-08-15T21:35:15.850Z
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
CC BY-SA 4.0
2020-08-15T21:54:19.117Z
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
CC BY-SA 4.0
2020-08-15T21:55:32.287Z
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
CC BY-SA 4.0
2020-08-15T22:02:19.277Z
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
CC BY-SA 4.0
2020-08-15T22:03:07.087Z
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
CC BY-SA 4.0
2020-08-15T22:34:42.557Z
I added an explanation on how to get heterogenous lists. I am convinced you're doing the wrong thing. It looks like you're analyzing sentences into lists of tokens whose types indicate their grammatical roles. It would seem wise to have a more elaborate structure than a list, and a type whose elements are grammatical roles. You can always map those to the corresponding types.
Andrej Bauer
CC BY-SA 4.0
2020-08-15T22:36:07.547Z
30 is a small number. You are aproximating it with infinity when you say you need "arbitrary types". Is there something in grammar that corresponds to the type $((t \to e) \to t) \to (e \to t)$? If not, why do you want that type?
Andrej Bauer
CC BY-SA 4.0
2020-08-15T22:39:16.060Z
There are things much much more complicated than that type in natural language, yes. But perhaps I could work with a small fragment and expand when possible.
user65526
CC BY-SA 4.0
2020-08-15T22:40:21.220Z
It looks like something [like this](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/grammatical-framework/09C4B3F43447ADDB0F632C64F195BC9C) is relevant to your work.
Andrej Bauer
CC BY-SA 4.0
2020-08-15T22:46:55.727Z
Yes, it is, thanks. I've come across some of the work he did in the early 90s, using Martin Löf type theory for natural language semantics.
user65526
CC BY-SA 4.0
2020-08-15T21:23:21.313Z
2020-08-15T22:33:02.997Z
2020-08-15T22:33:02.997Z
Andrej Bauer
<p>Suppose we have a set <span class="math-container">$S$</span> of constants of the Simply-Typed Lambda Calculus (STLC) various types, and the operation of union <span class="math-container">$\cup$</span> which takes two constants and forms their union.</p>
<p>For example, <span class="math-container">$S$</span> could be <span class="math-container">$\{\, a_e, b_e, f_{e \to t}, g_{e \to e \to t}\}$</span>, where <span class="math-container">$e$</span> and <span class="math-container">$t$</span> are ground types of the STLC and <span class="math-container">$e \to t$</span> is a function type. We can then form <span class="math-container">$\{a, g, b \}$</span>, by unioning <span class="math-container">$a$</span>, <span class="math-container">$g$</span> and <span class="math-container">$b$</span>. We could do this iteratively, first unioning <span class="math-container">$g$</span> and <span class="math-container">$b$</span>, and thence <span class="math-container">$a$</span>.</p>
<p>However, suppose we wanted to do this sort of iterative process in the STLC with ordered pairs, forming <span class="math-container">$(g, b)$</span> and then <span class="math-container">$(a, g, b)$</span>. One way might be to use the Kuratowski encoding of ordered pairs, and use union as before, as well as a singleton-forming operation <span class="math-container">$\zeta$</span>. We would therefore add to the STLC <span class="math-container">$\zeta$</span> and <span class="math-container">$\cup$</span>. In the Kuratowski encoding, <span class="math-container">$(a, g, b)$</span> is defined as <span class="math-container">$(a, (g, b))$</span>, which in turn is defined as <span class="math-container">$\{ \{a \}, \{ \{g \}, \{g, b \} \} \}$</span>.</p>
<p>Take <span class="math-container">$\{ \{g \}, \{g, b \} \}$</span>. We could form this by applying <span class="math-container">$\zeta$</span> to <span class="math-container">$g$</span> and <span class="math-container">$\zeta$</span> to <span class="math-container">$b$</span> and then unioning <span class="math-container">$\{g\}$</span> and <span class="math-container">$\{b \}$</span> to form <span class="math-container">$\{g, b \}$</span>, applying <span class="math-container">$\zeta$</span> to the result to form <span class="math-container">$\{ \{g,b \} \}$</span> and then applying <span class="math-container">$\zeta$</span> twice to <span class="math-container">$g$</span>, and unioning <span class="math-container">$\{ \{ g \}\}$</span> and <span class="math-container">$\{ \{g,b \} \}$</span>, to form <span class="math-container">$\{ \{g \}, \{g, b \} \}$</span>. Then a function of the following kind could be written:</p>
<p><span class="math-container">$$\lambda b, a. \zeta \, \zeta \,\zeta\, a \,\cup \,\zeta\,(\zeta\,\zeta\, g \cup \zeta\,(\zeta \,g\cup \zeta\,b)))$$</span></p>
<p>Another way would be to use the powerset monad, where</p>
<ul>
<li>the unit <span class="math-container">$\eta$</span> of the monad takes an element and forms a singleton</li>
<li>the join of the monad <span class="math-container">$\mu_A : \mathcal{P}(\mathcal{P}(A)) \to \mathcal{P}(A)$</span> is union, i.e., <span class="math-container">$\mu_A(S) = \bigcup_{B \in S} B$</span>.</li>
</ul>
<p>For <span class="math-container">$M \in \mathcal{P}(A)$</span> and <span class="math-container">$K : A \to \mathcal{P}(B)$</span> we have
<span class="math-container">$$M \star K = \bigcup_{x \in M} K(x) = \mu_A(\{K(x) \mid x \in M\})$$</span></p>
<p>We can compute the union of two subsets <span class="math-container">$X, Y \subseteq S$</span> as
<span class="math-container">\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*}</span></p>
<p>We could then form (a, g, b), by applying the <span class="math-container">$\bigstar$</span> iteratively, to create the Kuratowski encoding of <span class="math-container">$(a, g, b)$</span>.</p>
<p>However, both these constructions have to go through the laborious detour of forming a set which, by the Kuratowski encoding, constitutes an ordered pair.</p>
<p>I am looking for a monad or applicative which allows us to form tuples such as <span class="math-container">$(a, g, b )$</span> in a more direct way than the ways just described, or simply in an alternative way.</p>

CC BY-SA 4.0
2020-08-15T19:32:02.143Z
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
CC BY-SA 4.0
2020-08-15T20:45:07.850Z
@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
CC BY-SA 4.0
2020-08-15T20:48:48.280Z
@Andrej Bauer, yes, correct, and they are supposed to be lambda terms of different types. Section 2.1 of this https://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
CC BY-SA 4.0
2020-08-15T21:10:31.000Z
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
CC BY-SA 4.0
2020-08-15T21:12:00.973Z
If the answer "You are looking for the [list monad](https://en.wikibooks.org/wiki/Haskell/Understanding_monads/List)]" 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
<type-theory><lambda-calculus><ct.category-theory><monad><applicative>
Forming ordered pairs using monads and doing without the Kuratowski encoding of ordered pairs
user65526
# Forming ordered pairs using monads and doing without the Kuratowski encoding of ordered pairs

(Asked by: username_0 on 2020-08-15)

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.

**Tags:** type-theory, lambda-calculus, ct.category-theory, monad, applicative

> **Comments:**
> **username_1**: 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?  
> **username_0**: @username_1 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.  
> **username_0**: @username_1, yes, correct, and they are supposed to be lambda terms of different types. Section 2.1 of this https://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.  
> **username_1**: 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.  
> **username_1**: If the answer "You are looking for the [list monad](https://en.wikibooks.org/wiki/Haskell/Understanding_monads/List)]" 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.  

---

## 1 answers

### Answer by username_1 on 2020-08-15. Score: 0

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](http://hackage.haskell.org/package/base-4.12.0.0/docs/src/GHC.Base.html#line-984).

**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](https://en.wikipedia.org/wiki/Dependent_type#%7F%27%22%60UNIQ--postMath-00000012-QINU%60%22%27%7F_type) $\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$.

> **Comments:**
> **username_0**: 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.  
> **username_1**: 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.  
> **username_1**: I think the original sin here is that you're introducing constants of arbitrary types. That feels like the wrong level to me.  
> **username_0**: 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.  
> **username_0**: 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.  
> **username_1**: I added an explanation on how to get heterogenous lists. I am convinced you're doing the wrong thing. It looks like you're analyzing sentences into lists of tokens whose types indicate their grammatical roles. It would seem wise to have a more elaborate structure than a list, and a type whose elements are grammatical roles. You can always map those to the corresponding types.  
> **username_1**: 30 is a small number. You are aproximating it with infinity when you say you need "arbitrary types". Is there something in grammar that corresponds to the type $((t \to e) \to t) \to (e \to t)$? If not, why do you want that type?  
> **username_0**: There are things much much more complicated than that type in natural language, yes. But perhaps I could work with a small fragment and expand when possible.  
> **username_1**: It looks like something [like this](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/grammatical-framework/09C4B3F43447ADDB0F632C64F195BC9C) is relevant to your work.  
> **username_0**: Yes, it is, thanks. I've come across some of the work he did in the early 90s, using Martin Löf type theory for natural language semantics.  

---

