# A monad that unions sets

Suppose we have a monad that maps types of some kind to other types (see below) , and let types be sets. Let $$\alpha, \beta$$ be types, $$\rightarrow$$ denote a function between types, and let $$a : \alpha$$ indicate that $$a\hspace{0.2cm}$$ (or $$b$$) is an expression of type $$\alpha$$.

Suppose $$a : \alpha \hspace{0.2cm}$$ indicates that $$a$$ is in the set of $$\alpha$$'s (for example, the set of truth values, individuals, etc). Thus $$a: \alpha \to \beta$$ means that $$a$$ is in the set of functions from $$\alpha$$ to $$\beta$$. Let type $$t$$ be the type of boolean truth values. Then the powerset monad can be described as on p.286 https://arxiv.org/pdf/cs/0205026.pdf, as a structure $$\thinspace(\mathbb{M}, \eta, \bigstar)\thinspace$$, with $$\eta$$ the unit and $$\bigstar$$ the binary operation of the monoid) such that:

$$\mathbb{M} \thinspace α = (α → t) \hspace{1cm} ∀α$$ $$η(a) = \{a\} : \mathbb{M} \thinspace α \hspace{1cm} ∀a : α$$ $$m \bigstar k = \bigcup_{a \in m} k(a): \mathbb{M}\thinspace β \hspace{1cm} ∀m : \mathbb{M}\thinspace α,\; k : α → \mathbb{M}\thinspace β .$$

I am looking for a monad which is a little like this, except that $$\eta$$ applied to an expression $$a$$ is the singleton containing $$a$$, but where $$\eta(a) \bigstar k$$ forms the union set $$\{a, \; k\}$$, so $$\bigstar$$ unions together sets. How would I define such a monad, in the kind of format above?

Basically, I'm looking for a monad which allows you to form singleton sets, and then union them together into one set.

$$Clarification$$: I just wondered whether there is $$some$$ monad which provides an operation that unions $$\{ John \}$$ and $$\{ sleeps \}$$. Perhaps it is not the power set monad, but another monad.

The application I have in mind relates to binary trees in linguistics: consider a binary branching tree, with $$\{x\}$$ on one branch $$B_1$$ and $$\{k\}$$ on the adjacent branch $$B_2$$. $$x∈Dom(k)$$ but we have 'lifted' both $$x$$ and $$k$$ to their singleton sets (see the picture below). Now we use some function which looks at the node with $$\{x\}$$ on one branch and $$\{k\}$$ on the adjacent branch and then forms $$\{k,x\}$$ on the mother node of $$B_1$$ and $$B_2$$, where $$k$$ for example is a constant of type $$\alpha \to \beta$$ and $$x$$ is a constant of type $$\alpha$$.

In the application I am considering, we let $$e, t$$ and $$s$$ be any three objects, none of which is an ordered pair, and then the set of types is the smallest set $$T$$ satisfying: (1) $$e, t, s \in T$$; (2) $$\alpha, \beta \in T$$ implies $$\alpha \to \beta \in T$$. Objects of type $$e$$ are individuals, objects of type $$t$$ are Boolean truth values and objects of type $$s$$ are possible worlds or indices and objects of type $$\alpha \to \beta$$ are functions from objects of type $$\alpha$$ to objects of type $$\beta$$. Then terms of the logic are given a type and the terms denote objects in a domain (a set of things). So a term of type $$e$$ denotes an object in $$D_e$$, the domain of individuals, and a term of type $$e \to t$$ denotes an object in $${D_t}^{D_e}$$, the set of functions from individuals to truth values. This is just Church's simply theory of types with an extra type $$s$$.

I believe that the sort of tree I am thinking of can be represented as the power of the two images below, with $$\bigstar$$ operating first on $$\{false, true \}$$ (the unary branch) and then $$\{false, true\}$$ taking the lambda term on the adjacent branch. If someone could confirm this is correct, that would be great.

If I understand correctly, the choice of $$false$$ and $$true$$ is not necessitated, though it might be natural in certain circumstances.  • The expression $\{a, k\}$ is ill-typed: a is an element, but k is a function. For example, $\{1,3,4\}$ is a set of numbers but $\{1, (x \mapsto \{i \in \mathbb{R}| i \leq x\}) \}$ is a set of what? Perhaps you meant something else? – Musa Al-hassy Oct 22 '18 at 18:47
• You will presumably need to solve $({\mathbb M}(\alpha)\to t)={\mathbb M}(\alpha)$ for that. – მამუკა ჯიბლაძე Oct 22 '18 at 20:23
• @ Musa Al-hassy Why can't the set contain different kinds of things? (i.e, normally we can have a set which contains a function and an element.) – user65526 Oct 22 '18 at 20:59
• @ მამუკა ჯიბლაძე Sorry, I don't understand what you mean. – user65526 Oct 22 '18 at 21:00
• I wanted to say that most likely your requirement forces to have all kind of things like $\{a,\{b,\{c,d\}\},\{e,\{f,\{g,\{h,k\}\}\}\},...\}$ so that you will need all iterates of the powerset – მამუკა ჯიბლაძე Oct 22 '18 at 22:41

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

You presented the monad in another way, using the bind operation $$\star$$ instead of the monad multiplication. But $$\mu$$ and $$\star$$ are expressible in terms of each other. 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\})$$ and for $$S \in \mathcal{P}(\mathcal{P}(A))$$ we have $$\mu_A(S) = \bigcup_{B \in S} B = S \star \mathbf{id}_{\mathcal{P}(A)}.$$

For instance, we can compute the union of two subsets $$X, Y \subseteq A$$ 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*}$$ You might object to my using the set $$\{\mathbf{false}, \mathbf{true}\}$$ but note that we have to use something specific to the monad in question, or else we can only write down expressions that work for all monads, and that will make it impossible to do anything interesting with our monad. Indeed, an expression which involves only $$\star$$ and $$\eta$$, and nothing else specific to the powerset monad, will only ever generate singletons.

The powerset monad is used to model non-determinism in programming. There we usually equip it with an additional operation that allows us to create a non-singleton set. So perhaps this is what you're asking for?

• I don't understand how $S \bigstar \eta_{A}$ is well typed. $S \in \mathcal{P}(\mathcal{P}(A))$ and $\eta_{A} \in A \to \mathcal{P}(A)$ but then $\bigstar \in \mathcal{P}(\mathcal{P}(A)) \to [\mathcal{P}(A) \to \mathcal{P}(A)] \to \mathcal{P}(A)$. But the function between $`[\,]'$ is not the type of $\eta_{A}$. – user65526 Oct 24 '18 at 21:41
• I'm not sure this is what I am looking for, since I want a function which takes two different singleton sets and then forms the union of those two sets. So the function acts on singleton sets. – user65526 Oct 24 '18 at 21:55
• Oops, good catch. That $\eta$ should have been the identity function. I hope it type-checks now. I also added an explanation on how to compute the union of two sets. – Andrej Bauer Oct 25 '18 at 6:24
• I don't understand how $\{\mathbf{false}, \mathbf{true}\} \star (\lambda b : \mathbf{bool} \,.\, \mathbf{if}\,b\,\mathbf{then}\,X\,\mathbf{else}\,Y)$ unions $X$ and $Y$. Could you explain this lambda term? The application I have in mind: consider a binary branching tree, with $\{x \}$ on one branch and $\{k\}$ on the adjacent branch. $x \in Dom(k)$ but we have 'lifted' both x and k to their singleton sets. Now we use some function which looks at the node with $\{x \}$ on one branch and $\{k\}$ on the adjacent branch and then forms $\{k, x \}$, where $k, x \in TYPE$. – user65526 Oct 25 '18 at 8:58
• I have clarified my question above. – user65526 Oct 25 '18 at 9:23