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.

`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? $\endgroup$ – Musa Al-hassy Oct 22 '18 at 18:47