Here is a shorter proof that right-occlusive implies left-occlusive. b >>= const a = join (fmap (const a) b) monad law (=<<) = (join.).fmap = join (const (return a) b) assumption: left-occlusive = join (return a) = a monad law join.return = id I still don't know whether right-occlusive implies left-occlusive. But I found a non-commutative monad which is not a reader monad and which is left-occlusive: the Set monad from the infinite-search package [1]. This monad is non-trivial and quite obviously satisfies fmap.const = const.return when you look at the source of the Functor instance. I verified by timing search over a vast and a tiny Set. In accordance with your arguments, I am beginning to think that b >> a = a could be taken as a _definition_ of a side-effect-free monad. Cheers, Olaf [1] http://hackage.haskell.org/package/infinite-search On Thu, 2020-11-12 at 16:25 -0500, David Feuer wrote:

First, for clarity, note that

const id = flip const

Consider a (right-)occlusive functor. We immediately see that

liftA2 (flip const) m (pure x) = pure x

Using the Applicative laws, we can restate this:

x <$ m = pure x

We get the same sort of result for a left-occlusive effect.

So an occlusive effect can't have any *observable* side effects. It must be "read only".

On Thu, Nov 12, 2020, 3:59 PM Olaf Klinke wrote:

...

...

First, instead of `const id` I will use `const`, that is, we shall prove

const = liftM2 const :: M a -> M b -> M a

which I believe should be equivalent to your property.

My belief was wrong, which is evident when using do-notation. Kim-Ee stated

do {_ <- b; x <- a; return x} = a

while I examined

do {x <- a; _ <- b; return x} = a

Since do {x <- a; return x} = a holds for any monad, Kim-Ee's property can be reduced to

do {_ <- b; a} = a or more concisely b >> a = a

which I called Kleisli-const in my previous post. As we seemed to have settled for "occlusive" I suggest calling b >> a = a "right-occlusive" or "occlusive from the right" because the right action occludes the side-effects of the left action, and do {x <- a; _ <- b; return x} = a should be called "left-occlusive" or "occlusive from the left" because the left action hides the effect of the right action. Under commutativity, both are the same but in general these might be different properties. I do not have a distinguishing counterexample, though, because all monads I come up with are commutative.

David Feuer hinted at the possibility to define occlusiveness more generally for Applicative functors. Commutativity might be stated for Applicatives as

liftA2 f a b = liftA2 (flip f) b a

So far I can only see two classes of occlusive monads: The reader- like (Identity ~ Reader ()) and the set-like monads.

Olaf

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.