1
$\begingroup$

$\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.

$\endgroup$
10
  • 2
    $\begingroup$ I added a definition but I don't know if it's exactly what you have in mind. I suggest that in the future you try to include definitions of your terms so that your questions are self-contained. $\endgroup$ – Gabriel C. Drummond-Cole Jan 29 '18 at 17:04
  • $\begingroup$ Sure! A domain is an algebra for the identity monad on the category of domains :-P. On a more serious note, I had the impression that the role of domains in computer science was not typically as a data structure, but rather as a place for the semantics of a language to take values. Are you sure you want a "domain" data structure? Note also that the "nonalgebraic" nature of the definition of a domain (saying there exist upper bounds but not specified upper bounds) is not very monad-friendly. $\endgroup$ – Tim Campion Feb 27 '18 at 17:44
  • 1
    $\begingroup$ Taking seriously the beginning of the comment by @TimCampion, I'd suggest that the question would be a lot clearer if you said what category you want the dcpo's to be monadic over. From "like a tree with extra axioms" (in your question), I would guess that you might be thinking of some forgetful functor from dcpo's to trees and asking whether that's monadic. On the other hand, I see no nontrivial functor from dcpos's to trees (i.e., I don't see how dcpo's are like trees), so maybe you meant something entirely different by that "like trees" remark. $\endgroup$ – Andreas Blass Feb 27 '18 at 18:15
  • 2
    $\begingroup$ Duplicate of math.stackexchange.com/questions/2654381/the-domain-comonad in case that's relevant. $\endgroup$ – Andrej Bauer Feb 27 '18 at 20:03
  • 1
    $\begingroup$ I find it unlikely you will be able to find a reasonable functor. Perhaps someone else can have a positive suggestion, but at least I don't see how to rescue your question. $\endgroup$ – Andrej Bauer Feb 28 '18 at 13:40
1
$\begingroup$

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)

$\endgroup$
2
  • 2
    $\begingroup$ Regarding the last paragraph, it's true that the forgetful functor to sets is not monadic, because it does not reflect isomorphisms. A simple example is the evident poset bijection from $a \leq c \geq b$ to $0 \leq 1 \leq 2$, which preserves directed joins. $\endgroup$ – Todd Trimble Jan 25 at 15:54
  • 1
    $\begingroup$ @ToddTrimble Great example. My intuition from other lattices led me to guess that bijections are isomorphisms, but I see now that's very wrong! $\endgroup$ – Andrew Dudzik Jan 25 at 16:08
-1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.