A monad that unions sets

Question

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.

Answer 1

The powerset monad that you describe already does precisely what you are asking for:

• 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?