[Haskell-cafe] What to call Occult Effects

[Olaf Klinke]

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 <olf at aatal-apotheke.de>
> 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.