The canonical 'Monad instance' for environment sharing plus nondeterminism is as follows (using pseudo-Haskell, since Haskell's Data.Set
isn't, of course, monadic):
eta :: a -> r -> {a} -- '{a}' means the type of a set of a's
eta x = \r -> {x}
bind :: (r -> {a}) -> (a -> r -> {b}) -> r -> {b}
m `bind` f = \r -> {v | x ∈ m r, v ∈ f x r}
Generally, when trying to combine a 'container' monad like Powerset (List, Writer, etc) with a second monad m
(here, roughly, Reader), one 'wraps' m
around the container monad, as done above.
I wonder, then, about the following potential Powerset-over-Reader specification:
eta' :: a -> {r -> a}
eta' x = {\r -> x}
bind' :: {r -> a} -> (a -> {r -> b}) -> {r -> b}
m `bind'` f = {rb | x <- m, ∀r: ∃rb' ∈ f (x r): rb r == rb' r}
This doesn't seem obviously crazy (I do realize that GHCi can't check rb r == rb' r
for many rb
and rb'
), but bind'
is complicated enough to make it difficult (for me) to check whether the monad laws hold.
My question, then, is whether eta'
and bind'
really are monadic -- and, if not, which of the law(s) is violated, and what sort of unexpected behavior might this correspond to?
A secondary question, assuming that eta'
and bind'
aren't monadic, is how one might ascertain whether there are functions with these types that are?
Fun question. Here is my take -- let's see if I didn't goof anywhere!
To begin with, I will spell your signatures in (slightly less pseudo) Haskell:
Before continuing, it is worth mentioning two practical complications. Firstly, as you have already observed, thanks to
Eq
and/orOrd
constraints it is non-trivial to give setsFunctor
orMonad
instances; in any case, there are ways around it. Secondly, and more worryingly, with the type you propose for(>>=)
it is necessary to extracta
s fromPSet (r -> a)
without having any obvious supply ofr
s -- or, in other words, your(>>=)
demands a traversal of the function functor(->) r
. That, of course, is not possible in the general case, and tends to be impractical even when possible -- at least as far as Haskell is concerned. In any case, for our speculative purposes it is fine to suppose we can traverse(->) r
by applying the function to all possibler
values. I will indicate this through a hand-wavyuniverse :: PSet r
set, named in tribute to this package. I will also make use of anuniverse :: PSet (r -> b)
, and assume we can tell whether twor -> b
functions agree on a certainr
even without requiring anEq
constraint. (The pseudo-Haskell is getting quite fake indeed!)Preliminary remarks made, here are my pseudo-Haskell versions of your methods:
Next, the monad laws:
(By the way, when doing this sort of thing it is good to keep in mind the other presentations of the class we are working with -- in this case, we have
join
and(>=>)
as alternatives to(>>=)
-- as switching presentations might make working with your instance of choice more pleasant. Here I will stick with the(>>=)
presentation ofMonad
.)Onwards to the first law...
One down, two to go.
return y >>= f
, therefore, might possibly be a much larger set thanf y
. We have a violation of the second law; therefore, we don't have a monad -- at least not with the instance proposed here.Appendix: here is an actual, runnable implementation of your functions, which is usable enough at least for playing with small types. It takes advantage of the aforementioned universe package.