Add AccumT

[turion]

I've checked the laws for MMonad by hand and I think they are satisfied. Might have made a mistake though. The iffy part is where we reuse the first environment for both actions, since we don't have the inner environment available yet. This is similar to StateT, except that for AccumT we can still combine the environments.

Compatibility with Monad

I have the feeling that MMonad instances should satisfy another law not documented yet. embed should be related to >>= in some way, but I'm not sure in what way precisely. You say that embed is "analogous" to >>=. It does indeed replicate it, and I think there should be a precise way to say that.

Candidate law

Recall:

(=<<) :: (a -> t n b) -> t n a -> t n b
embed :: (forall x . m x -> t n x) -> t m b -> t n b

Let:

nat :: forall x . n x -> t n x
m :: t n b

Then we require:

nat . return =<< m = embed nat m

An example for nat might be lift, but there are others like \m -> ask >>= print >> lift m :: IO x -> ReaderT Int IO x, or const $ throwE e :: m x -> ExceptT e m x. I'm not sure whether nat is simply a natural transformation or a monad morphism though. (My first example isn't one.)

Relevance to AccumT

I believe that such a law would be broken for my instance, because in the Monad instance for AccumT the emission of later environments is influenced by earlier ones. So this MMonad instance is probably surprising and maybe shouldn't be merged.

[Gabriella439]

@turion: So, if nat were a monad morphism, then in this equation:

nat . return =<< m = embed nat m

… nat . return would equal return (by the monad morphism laws), which would give:

return =<< m = embed nat m

… and since return =<< m = m, then that would simplify further to:

m = embed nat m

… which does not hold in general. In fact, it only holds for lift (and since lift is the identity of <|< and the identity morphism is necessarily unique up to isomorphism, then lift is the only solution for nat).

But anyway, I still think this is fine to merge regardless, because AccumT is "morally" the same as WriterT and this instances behaves the same as the MMonad instance for WriterT

[turion]

Candidate law

That's a great observation! I can't follow why m = embed nat m doesn't hold for a general monad morphism. (I agree it doesn't hold for every natural transformation.) For t a given monad transformer and n a given monad, what other monad morphisms forall x . n x -> t n x besides lift are there? Maybe you have an example handy? I can't think of any that would survive the law nat m >> nat m = nat (m >> m).

MMonad AccumT

I think I have an example where I can boil down my issue with the proposed instance. The only difference between AccumT and WriterT is that AccumT has a function look :: AccumT w m w which retrieves the current log. And this behaves differently in embed than in =<<, because in embed we pass the same log to both parts, whereas in cont =<< action, cont receives the updated log. Here's the example:

-- As an action, we add 1 to the log
>>> let action = add $ Sum 1
-- Read the current log and print it. This is a natural transformation, but not a monad morphism.
>>> let nat m = look >>= lift . print >> m
-- `runAccum` gives us the return value of the monad, and the accumulated log.
-- We've accumulated a log of `Sum 1` at the end of `action`.
>>> runAccum action $ Sum 0
((),Sum {getSum = 1})
-- Let's run the effects of `nat` (printing the current log) after `action`.
-- As expected, the current log after `action` is `Sum 1`.
>>> runAccumT (action >> nat (return ())) $ Sum 0
Sum {getSum = 1}
((),Sum {getSum = 1})
-- Whoops! `nat` is executed after `action`, but the updated log is not forwarded to it! It's still 0 while `nat` is running.
-- Only at the end we get the updated log.
>>> runAccumT (embed nat action) $ Sum 0
Sum {getSum = 0}
((),Sum {getSum = 1})

[turion]

Side note, feel free to disregard

Another viewpoint is that join :: t m (t m a) -> t m a and squash :: t (t m) a -> t m a must be related.

Recall:

(=<<) :: (a -> t n b) -> t n a -> t n b
cont =<< action = join $ fmap cont action
embed :: (forall x . m x -> t n x) -> t m b -> t n b
embed nat action = squash $ hoist nat action

Let's express the proposed law in terms of join and squash:

nat . return =<< m = embed nat m
-- Insert identities for `=<<` and `embed`
join $ fmap (nat . return) m = squash $ hoist nat m
-- This should hold for any m
join . fmap (nat . return) = squash . hoist nat

Expressing it like this is a bit nicer because there is only one free variable, nat. I don't know whether this can be simplified any more. (I couldn't find a way to express join in terms of squash or the other way around, although it feels a bit like join should be expressible in terms of squash in some situations. But maybe I'm imagining too much.)

Either way this is trivially satisfied for lift.

One might think that doesn't make much sense to require this law for anything else than a monad morphism because hoist requires nat to be a monad morphism. But I don't see why, to be honest. There are a lot of meaningful constructions which are instances of MFunctor which don't produce monads. (They should be FFunctors probably, though.)

[Gabriella439]

@turion: Here is the more direct proof of why embed nat m = m implies that nat = lift

Since the equation must be true for all m, replace m with lift x:

embed nat (lift x) = lift x

… according to the MMonad class laws: embed f (lift m) = f m, so the above equation simplifies further to:

nat x = lift x

… and by η-reduction, you get:

nat = lift

The same property is true for the other equation you proposed: nat must necessarily be lift.

Also, looking more closely at the MMonad instance for AccumT, I think it does not satisfy the MMonad laws anyway so we don't need to invoke any new laws to reject the instance. Specifically, I don't believe it satisfies this law:

embed f (lift m) = f m

This is because:

embed f (lift m)

= A.AccumT $ \w -> do
    ((b, wInner), wOuter) <- A.runAccumT (f $ A.runAccumT (lift m) w) w
    return (b, wInner `mappend` wOuter)

= A.AccumT $ \w -> do
    ((b, wInner), wOuter) <- A.runAccumT (f $ fmap (, mempty) m) w
    return (b, wInner `mappend` wOuter)

… and the latter expression does not necessarily equal f m for all possible definitions of f

[turion]

@turion: Here is the more direct proof of why embed nat m = m implies that nat = lift

Yes, that part I believe. But I don't believe my proposed law is equivalent to embed nat m = m when nat is not a monad morphism. (In particular it doesn't mention >>=.) Maybe it feels weird to state the law for nat not a monad morphism, but in practice one will often apply embed to things that are not monad morphisms.

Also, looking more closely at the MMonad instance for AccumT, I think it does not satisfy the MMonad laws anyway so we don't need to invoke any new laws to reject the instance. Specifically, I don't believe it satisfies this law:

embed f (lift m) = f m

This is because:

embed f (lift m)

= A.AccumT $ \w -> do
    ((b, wInner), wOuter) <- A.runAccumT (f $ A.runAccumT (lift m) w) w
    return (b, wInner `mappend` wOuter)

= A.AccumT $ \w -> do
    ((b, wInner), wOuter) <- A.runAccumT (f $ fmap (, mempty) m) w
    return (b, wInner `mappend` wOuter)

… and the latter expression does not necessarily equal f m for all possible definitions of f

I think it does:

= A.AccumT $ \w -> do
    ((b, wInner), wOuter) <- A.runAccumT (f $ fmap (, mempty) m) w
    return (b, wInner `mappend` wOuter)
-- naturality
= A.AccumT $ \w -> do
    ((b, wInner), wOuter) <- A.runAccumT (fmap (, mempty) $ f m) w
    return (b, wInner `mappend` wOuter)
-- fmap & monad law
= A.AccumT $ \w -> do
    (b, wOuter) <- A.runAccumT (f m) w
    return (b, mempty `mappend` wOuter)
-- monoid
= A.AccumT $ \w -> do
    (b, wOuter) <- A.runAccumT (f m) w
    return (b, wOuter)
-- monad law
= A.AccumT $ \w -> do
    A.runAccumT (f m) w
-- newtype erasure
= f m

[Gabriella439]

Oh, you're right, I forgot about naturality

Then I think this MMonad instance is probably fine.

My interpretation of the example you gave is when you said that "nat is executed after action" I think the way you phrased that is the root of the misunderstanding. When you write f =<< (action :: t m a), f is "after" action in the sense that f depends on an input of type a : Type. However, when you write embed f (action :: t m a), f is "after"action in the sense that f depends on an "input" of type m :: Type -> Type. In the latter case, f doesn't actually depend on the a at all (it's natural in a, as you noted), so the fact that it ignores the current state of the log actually makes sense to me.

I think it would make more sense if I gave an example using a different monad / monad morphism. Let's use the following contrived example:

-- The `MaybeT` layer is not actually used, yet
example :: MaybeT [] (Int, Int)
example = do
    x <- lift [ 1, 2, 3 ]
    y <- lift [ 4, 5, 6 ]
    return (x, y)

-- listToMaybeT is a monad morphism (proof omitted)
listToMaybeT :: Monad m => [a] -> MaybeT m a
listToMaybeT (x : _) = pure x
listToMaybeT  []     = empty

result :: MaybeT Identity (Int, Int)
result = embed listToMaybeT example

Now, in the case of result, the embed is not acting on any of the results, meaning that it does not affect x, y, or (x, y). Instead, embed is acting on the lifts. We can see this if we expand out result using equational reasoning, which (I believe) should eventually give:

result = do
    x <- listToMaybeT [ 1, 2, 3 ]
    y <- listToMaybeT [ 4, 5, 6 ]
    return (x, y)

You can build an intuition for how this works by thinking of embed as the "lift-substitution" function, meaning that embed f action replaces all of the lifts in action with f. In this light, the first two MMonad laws for embed can be read as saying:

-- Replacing all `lift`s with `f` within the expression `lift m` gives `f m`
embed f (lift m) = f m

-- Replacing all `lift`s with `lift` does nothing
embed lift m = m

Also, by analogy, you can think of =<< as the "return-substitution" function.

So if you think of embed as operating at a higher kind by operating on lifts, then in my eyes makes sense that it's unaware of what is happening to the result at a lower kind.

So, although =<< and embed are similar in that they are substitution functions for their respective identities (return and lift), they operate at different kinds and therefore should not necessarily behave in the same way. This is why I don't think there should be an extra law relating the behavior of =<< and embed.

[turion]

Thanks a lot for this detailed and patient answer, that was a real eye-opener! The lift-substitution viewpoint is very helpful. I learned now that embed doesn't do anything like sequential composition, but rather it replaces every occurrence of m with t n (naturally). An extreme case might be FreeT f m, where we can have chains like f (m (f (m (..., and every m is replaced by a FreeT f n. So the FreeT f n parts are not executed "after" the FreeT f m parts at all.

In some special cases it happens that the transformer is constructed as t m a = m (f a) (ExceptT, WriterT) or t m a = g (m a) (ReaderT), and in this case one has t (t m) a = t m (f a) = m (f (f a)) or t (t m) a = g (t m a) = g (g (m a)) and then one can use the join of f or g to define squash. I think I was too focused on these examples.

StateT, AccumT, ListT, ContT, FreeT are all not of this form, so one cannot expect to derive an MMonad from Monad. But then "accidentally" (?) AccumT, ListT, FreeT happen have a lawful MMonad, so why not keep it.

[Gabriella439]

You're welcome! Also, thank you for contributing this change 🙂