Is Writer wrong?

[isovector]

IIRC @adamConnerSax was saying our Writer instance doesn't line up with MTL. Is this true, and if so, let's fix it.

[isovector]

It should be pass :: m (a, w -> w) -> m a instead of censor :: MonadWriter w m => (w -> w) -> m a -> m a in our algebra. But I couldn't figure out how to encode that in polysemy, but also I didn't try very hard.

[KingoftheHomeless]

I'll look into this.

[KingoftheHomeless]

Huh. This is very interesting.

Yes, from what I can tell, it's not possible to implement pass in Polysemy with semantics that reflect the one that censor has today. This is because the modifying function is wrapped in the functorial state, so you can't use it unless you use the inspector. You could implement pass by trying to extract the function with the inspector, and not do any censoring if the inspector fails, but that would mean censor implemented in terms of pass can fail to apply the censoring, which is not the case today when Writer is interpreted through runWriter.

But here's the thing: the semantics of Polysemy's censor differ from that of MTL, because MTL has exactly the same problem of the modifying function being wrapped inside a possibly failable computation, and if it fails, it won't apply the censoring!

Compare:

import Polysemy
import Polysemy.Writer
import Polysemy.Error

import Control.Monad.Except
import qualified Control.Monad.Writer.Class as MTL

one :: (String, Either () ())
one = runExceptT $
  do
    MTL.tell "censoring"
    MTL.censor (drop 4) (MTL.tell " not applied" *> throwError ())
      `catchError`
      (\_ -> pure ())
-- one == ("censoring not applied", Right ())

two :: (String, Either () ())
two =
    run
  . runWriter
  . runError
  $ do
    tell "censoring"
    censor (drop 4) (tell " not applied" *> throw ())
      `catch`
      (\_ -> pure ())
-- two == ("censoring applied", Right ())

So to sum it up, we can work pass into Writer, with the same semantics as MTL's pass,
but the semantics of censor will also be changed to that of MTL's censor.

[ocharles]

haskell/mtl#5 (comment) suggests a law for pass - does this explain the behavior above at all? It may be that WriterT (ExceptT e m) shouldn't exist

[KingoftheHomeless]

This is not WriterT s (ExceptT e m), but rather ExceptT e (WriterT s m) (more specifically, ExceptT () ((,) String).

Whatever the case, we can only have pass in the Writer effect if we're willing to follow MTL semantics.

[ocharles]

Right, I meant MonadWriter (ExceptT e m), not WriterT (ExceptT e m).

Whatever the case, we can only have pass in the Writer effect if we're willing to follow MTL semantics.

My point was there is also the option that mtl is wrong and this instance shouldn't exist. At that point what pass does when the inspector fails is less clear though, as there is nothing to copy - as mtl wouldn't let you write that.

[KingoftheHomeless]

Well, if we want pass, since we're implementing runWriter in terms of state anyway, the only other thing we could to is to roll-back the state if the inspector fails, so a failed computation won't do any tell-ing at all. But that would mean differing semantics for censor id body `catch` handler compared to body `catch` handler, so that's obviously insane.

[KingoftheHomeless]

Another alternative is to have separate effects for censor and pass, at the cost of the losing the equivalence censor f m = pass (fmap (, f) m)

[isovector]

Does anyone actually use pass? I never have.

[KingoftheHomeless]

Those MonadWriter laws in haskell/mtl#5 (comment) don't work out. Even (,) s violate them.

MTL.pass (("sim", ()) >>= \_ -> ("salabim", ((), id))) == ("simsalabim", ())
combine ("sim", ()) (\_ -> ("salabim", ((), id))) == ("simsimsalabim", ())

[ocharles]

Does anyone actually use pass? I never have.

https://codesearch.aelve.com/haskell/search?query=pass&filter=Control.Monad.Writer&insensitive=off&space=off&precise=off&sources=on only seems to show people defining pass.

[isovector]

@ocharles what is this sorcery? this thing exists??? it's like the answer to all of my prayers!

[ocharles]

😘

[KingoftheHomeless]

pass does have a motivating example: it's useful for conditional logging of an action that is decided by checking the result of that action.

To steal some (modified) code from StackOverflow:

deleteOn :: (Monoid w) => (a -> Bool) -> Writer w a -> Writer w a
deleteOn p m = pass $ do
    a <- m
    if p a
        then return (a, id)
        else return (a, const mempty)

It's only that it doesn't seem to crop up... at all?

[isovector]

That's a reasonable motivation. I'm inclined to go with the principle of least surprise here and just copy mtl's semantics. Any dissent on that front?

[ocharles]

Given how surprising it is and that we can't find any motivation, I'd rather drop it.

Edit: though does this mess up with the whole mtl-absorption stuff?

[isovector]

Just as an aside, it looks like Futhark is the sole user of this function in the whole world! https://codesearch.aelve.com/haskell/src/hackage/futhark/0.11.2/src/Futhark/CodeGen/Backends/GenericC.hs?query=pass&L=342#snippet.342

[KingoftheHomeless]

... Buuuuut it's a use that can be replaced with censor.

[KingoftheHomeless]

Hell, conditional logging can be achieved through censor too.

deleteOn :: (Monoid w) => (a -> Bool) -> Writer w a -> Writer w a
deleteOn p m = do
    (a, w) <- censor (const mempty) (listen m)
    when (p a) (tell w)
    return a

Perhaps there are some situations where pass is necessary, but I can't find one.

[KingoftheHomeless]

Actually, never mind, that kind of implementation is dangerous with current Polysemy semantics because if the action fails then the logging will always be deleted.

I dunno. I'm on the fence about this.

[KingoftheHomeless]

Actually, considering the issue with the deleteOn implementation under current polysemy semantics, I'm in favour of MTL semantics.
My thinking is that having censor always censor a failed action is too dangerous to be worth it. You can instead do that kind of censoring explicitly, even with MTL semantics.

censor' :: (MTL.MonadWriter s m, MonadError e m)
        => (s -> s)
        -> m a
        -> m a
censor' f m = do
  res <- MTL.censor f $ fmap Right m `catchError` (pure . Left)
  case res of
      Right res' -> return res'
      Left e -> throwError e

three :: (String, Either () ())
three = runExceptT $
  do
    MTL.tell "censoring"
    censor' (drop 4) (MTL.tell " not applied" *> throwError ())
      `catchError`
      (\_ -> pure ())
-- three == ("censoring applied", Right ())

[isovector]

Just to be clear, the semantics of polysemy today are completely accidental, and shouldn't be taken into consideration as "maybe these guys did it for a reason" :)

[KingoftheHomeless]

listen also has incorrect semantics. It doesn't commit the output it hears.

mtl :: (String, ((), String))
mtl = MTL.listen $ MTL.tell "yup"
-- mtl == ("yup", ((), "yup"))

polysemy :: (String, (String, ()))
polysemy = run . runWriter $ listen $ tell "yup"
-- polysemy == ("", ("yup", ()))

I'm going to add a pull request resolving this issue, together with adding pass.