The domain monad

Question

$\DeclareMathOperator\Set{\mathit{Set}}\DeclareMathOperator\Dom{\mathit{Dom}}\DeclareMathOperator\Hilb{\mathit{Hilb}}$Many different kinds of data structures can be captured as Monads. Lists and trees are two good examples. A domain (dcpo) is like a tree, with extra axioms.

Definition. A directed subset of a partially ordered set is a nonempty subset which contains an upper bound for every pair of elements in it. A domain or dcpo (directed-complete partial order) is a partially ordered set such that every directed subset has a supremum.

Can domains be encoded as a monad or comonad?

My intuition is telling me you can get both based on this paper.

One thought for the base category I would like to fix is $\Set$. So the functor $\Dom : \Set \rightarrow \Set $ maps a set to the set of all domains on that set. I am not sure how this functor works on morphisms. Another category of interest is $\Hilb$, so $\Dom_H : \Hilb \rightarrow \Hilb$. Below are some notes about $\Dom_H$.

It may be impossible to define such a monad, but we would need a proof.

[Edit] I am still trying to find a Domain monad. Tim Campion's suggestion about the base category is important. I suggested Set as the base, but Andrej Bauer has stated that it is unlikely to find a suitable functor. I am intrigued by Tim's comment that "there exists upper bounds" but they are not expressly defined. Perhaps the domain on Sets is a kind of abstract structure for the more specific domains we can define on more structured sets. To be precise, if we define the monad on structured objects, we can expressly state how to find upper bounds given a directed set. I am working from a physicist's perspective so I am thinking about Hilbert spaces. There is the spectral order as seen here and it forms a domain. They don't state how to compute upper bounds given a directed set, but perhaps this is a better, more concrete example where we can explicitly state how to comput upper bounds, thus making it a better candidate for a monad.

Answer 1

I'm not sure if this is exactly what you had in mind, but it's most natural to think of DCPOs as the algebras for the "ideals" monad over the category of partially ordered sets.

This should be a basic fact but it's surprisingly obscure in the literature. Jacob's Bases as Coalgebras has a proof in 4.1.

Here's how it works. For a poset $P$, an ideal is a nonempty directed subset $I\subset P$ such that $x\leq y \in I \implies x\in I$. The union of a directed system of ideals is an ideal, so the collection $\mathcal{I}(P)$ of all ideals is a DCPO, and in fact $\mathcal{I}$ extends to a monad on posets, with multiplication $\mathcal{I}^2(P) \to \mathcal{I}(P)$ given by union and unit $P\to \mathcal{I}(P)$ given by $y\mapsto \{x\leq y\}$.

It's not too hard to see that the algebras for this monad are just DCPOs. After all, any directed set generates an ideal, and a compatible morphism $\mathcal{I}(P) \to P$ is simply a directed join.

I don't know much about Hilbert spaces but I suspect that if you want to apply this result in that setting, you want to start with something like a poset of closed linear subspaces.

I think this is the best we can do; it shouldn't be hard to show that the forgetful functor $U:\rm{DCPO}\to\rm{Set}$ is not monadic using some version of Beck's monadicity theorem. I find it unlikely that $U$ plays well with coequalizers. (EDIT: As Todd Trimble points out, it's much easier than this, as $U$ does not even reflect isomorphisms)

Answer 2

I don't know.

However, if there were such a construction then it would need to be minimal in some sense and so it may help to google "initial object in the category of Id-algebras over DCP".

A stab in the dark would be to use multibranching trees where the order is the parent-child ordering,

-- i.e. rose trees
data Domain a = Embed a | Gather [Domain a] deriving (Functor, Eq) 

instance Eq a => Ord (Domain a) where

  -- the <= on (Domain a) is reflexive
  (Embed x  ) <= (Embed y)   =  x == y
  (Gather xs) <= (Gather ys) =  all (\(x,y) -> x <= y) (zip xs ys)

  -- leaf belongs to parent?
  (Embed x) <= (Gather ps)   = any (\p -> p == Embed x) ps

  -- otherwise no
  _ <= _ = False

instance Applicative Domain where
  pure  = Embed

  -- Essentially `map f xs`
  (Embed f) <*> (Embed x)       = Embed (f x)
  (Embed f) <*> Gather xs       = Gather $ map (\x -> Embed f <*> x) xs

  -- Evaluate all functions at `a`.
  (Gather fs)  <*>  (Embed a) = Gather $ map (\f -> f <*> Embed a) fs

instance Monad Domain where
  -- (>>=)       :: forall a b. Domain a -> (a -> Domain b) -> Domain b
  (Embed a) >>= f   = f a
  (Gather xs) >>= f = Gather $ map (\x -> x >>= f) xs

Whether the proofs-obligations go through is another matter.