Is the monad transformer of a monad unique in Haskell-CodePudding

There have been a couple of questions (e.g. this and this) asking whether every monad in Haskell (other than IO) has a corresponding monad transformer. Now I would like to ask a complementary question. Does every monad have exactly one transformer (or none as in the case of IO) or can it have more than one transformer?

A counterexample would be two monad transformers that would produce monads behaving identically when applied to the identity monad would but would produce differently behaving monads when applied to some other monad. If the answer is that a monad can have more than one transformer I would like to have a Haskell example which is as simple as possible. These don't have to be actually useful transformers (though that would be interesting).

Some of the answers in the linked question seemed to suggest that a monad could have more than one transformer. However, I don't know much category theory beyond the basic definition of a category so I wasn't sure whether they are an answer to this question.

CodePudding user response：

To make it short, no it can't. At least, if I am not wrong ;)

A Monad transformer should verify to the laws in Control.Monad.Trans. So if you consider the class of the Monad transformers defined by

class MonadTrans t where
-- | Lift a computation from the argument monad to the constructed monad.
lift :: Monad m => m a -> t m a

you may see that two laws have to be verified :

lift . return = return
lift (m >>= f) = lift m >>= (lift . f)

Consequently, consider a contrario that you have two different Monad transformers mT and mT' from the same monad m (so mT Identity = m and mT' Identity = m). I will annotate the function with _t to indicate the referenced class. Now, look at the first law. It ensures that

lift_mT . return_I = return_(mT I)
lift_mT' . return_I = return_(mT'I)

But, since mT Identity = m and mT' Identity = m, return_mTI = return_mT'I = return_m. Therefore

lift_mT . return_I = lift_mT' . return_I

Then lift_mT has to be equals to lift_mT'.

So, you can probably create two monad transformers that respect mT Identity = m and mT' Identity = m but that do not verify equality for monad n. However this means that at least one of your does not respect the first law.

CodePudding user response：

Here's one idea. We know that in general, monads don't compose... but we also know that if there's an appropriate swap operation, you can compose them[1]! Let's make a class for monads that can swap with themselves.

-- | laws (from [1]):
-- swap . fmap (fmap f) = fmap (fmap f) . swap
-- swap . pure = fmap pure
-- swap . fmap pure = pure
-- fmap join . swap . fmap (join . fmap swap) = join . fmap swap . fmap join . swap
class Monad m => Swap m where
    swap :: m (m a) -> m (m a)

instance Swap Identity where swap = id
instance Swap Maybe where
    swap Nothing = Just Nothing
    swap (Just Nothing) = Nothing
    swap (Just (Just x)) = Just (Just x)

Then we can build a monad transformer that composes a monad with itself, like so:

newtype Twice m a = Twice (m (m a))

Hopefully it should be obvious what pure and (<$>) do. Rather than defining (>>=), I'll define join, as I think it's a bit more obvious what's going on; (>>=) can be derived from it.

instance Swap m => Monad (Twice m) where
    join = fmap join . join . fmap swap

Now, we have

IdentityT Identity ~= Identity
IdentityT Maybe ~= Maybe

Twice Identity ~= Identity
Twice Maybe !~= Maybe

which shows that IdentityT is not a unique monad transformer for producing Identity.

[1] Composing monads by Mark P. Jones and Luc Duponcheel