3

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.

QuantumWiz
  • 66
  • 8
  • 1
    At some point I found myself needing a simple transformer I called [`OuterMaybeT`](https://github.com/leftaroundabout/manifolds/blob/6f4d3ed71497074ad4cef2874a2d9fe73a14a377/manifolds/Control/Monad/Trans/OuterMaybe.hs), which is different from `MaybeT` in general yet does give `OuterMaybeT Identity ≌ Maybe`. But only for applicative, I don't think it can be used as a monad transformer, and I actually never checked whether it's even law-abiding. – leftaroundabout Jun 03 '22 at 14:23
  • @leftaroundabout `OuterMaybe f` is just `Compose Maybe f`, isn't it? So it should be law-abiding as far as I can see. – amalloy Jun 03 '22 at 16:11
  • 1
    I mean we can trivially define a type `T` for which `T Identity ~= Maybe` and `T [] ~= []`, right? So... no, they're not unique. It's sort of a degenerate example, but then I can't really think of a clear property that would formalize my intuition about what I consider degenerate and what I don't. Maybe some sort of type-level analogue of parametricity or something...? – Daniel Wagner Jun 03 '22 at 16:23

3 Answers3

1

Here's one idea for a counterexample to uniqueness. 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 = id
        . Twice                        -- rewrap newtype
        . fmap join . join . fmap swap -- from [1]
        . runTwice . fmap runTwice     -- unwrap newtype

instance MonadTrans Twice where lift = Twice . pure

I haven't checked that lift obeys the MonadTrans laws for all Swap instances, but I did check them for Identity and Maybe.

Now, we have

IdentityT Identity ~= Identity ~= Twice Identity
IdentityT Maybe    ~= Maybe   !~= Twice Maybe

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

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

Daniel Wagner
  • 140,758
  • 9
  • 210
  • 370
  • But here, the monad transformer is `Twice` ? Isn't it ? And you provide a single definition of `Twice`. Am I wrong ? I mean you can say that `Swap` is also a monad transformer but you did not provide the `lift` function. – Benoît Fraikin Jun 03 '22 at 19:05
  • I think I misread your text. `IdentityT` and `Twice` are the monad transformers. So I will look at it. – Benoît Fraikin Jun 03 '22 at 19:28
0

To make it short, no it can't if you want to respect the laws of MonadTrans. 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.

Benoît Fraikin
  • 561
  • 4
  • 12
  • It's not clear to me that `lift_mT . returnI = lift_mT' . returnI` implies `lift_mT = lift_mT'`, and it's not clear to me that `lift_mT = lift_mT'` implies `mT = mT'`. – Daniel Wagner Jun 03 '22 at 17:58
  • For the part `lift_mT = lift_mT'` implies `mT = mT'` this is simply because the `lift` function defines the class instance. For the other part, for every function `f`, `g` and `h`, and every element `x`, if `g(f (x)) = h (f (x))` then `g(y) = h(y)` for every `y` in `Im(f)`. The only possibility to change will be in the domain of `g` and `h` that are not in `Im(f)`. But Identity is (as its name indicates) an isomorphism of `id`. – Benoît Fraikin Jun 03 '22 at 18:53
  • `lift` defines the `MonadTrans` class instance, but not the `Monad` instance. There are many types which have multiple possible `Monad` instances. Most monadic actions are not in `Im(return)`. – Daniel Wagner Jun 03 '22 at 18:56
  • @DanielWagner The MonadTrans is the class of all Monad transformation. If you are a Monad transformation you should be an instance of it. And your only definition that can characterize you is the `lift` function. – Benoît Fraikin Jun 03 '22 at 19:01
  • The uniqueness of instances is not a valid argument. You could rephrase the question without `MonadTrans` instance: are there two distinct transformers `T1` and `T2` with functions `lift1 :: Monad m => m a -> T1 m a` and `lift2 :: Monad m => m a -> T2 m a` both satisfying the `lift` laws? – Li-yao Xia Jun 03 '22 at 19:27
  • @BenoîtFraikin No, that's not correct. The definition of `>>=` can also characterize you (among other things). – Daniel Wagner Jun 03 '22 at 19:31
  • @DanielWagner I am sorry... but `>>=` characterize the structure as a monad and `lift` characterize the structure as a monad transformer. I understand from these discussion that you consider (not only you) that you don't need to instantiate MonadTrans to be a monad transformer. But this means that a monad should not need to instantiate Monad (and so `>>=`). And I don't think so. – Benoît Fraikin Jun 03 '22 at 19:43
  • @Li-yaoXia you define `lift` doesn't you ? So the problem is in the respect of the laws. And all my argumentation is about the laws... Isn't it ? – Benoît Fraikin Jun 03 '22 at 19:45
  • You have shown that the specializations of `lift_mT @Identity` and `lift_mT' @Identity` are equal. That does not imply that `lift_mT` and `lift_mT'` remain equal on arbitrary monads. – Li-yao Xia Jun 03 '22 at 19:56
  • @Li-yaoXia Oh ok. I see where there is a caveat. Thank you. I will sleep on that ;) – Benoît Fraikin Jun 03 '22 at 20:04
  • @BenoîtFraikin Certainly a monad transformer should instantiate `MonadTrans`. I can't understand any other part of your latest comment, so I can't agree or disagree. I will say this: if somebody wrote down two monad transformers with identical definitions of `lift` but different definitions of `>>=`, I would not consider those two transformers equal. I'm not sure if that's relevant to the latest part of the discussion or not. – Daniel Wagner Jun 03 '22 at 20:24
  • @DanielWagner I understand your point and I can indeed see what's my error. However this does not change that `lift` alone defines what kind of monad transformer like `mempty` and `mappend` define what kind of monoid it is. This is quite an interesting discussion. However I don't think this is a place. Thank you for the time and feedback (and @Li-yaoXia too) – Benoît Fraikin Jun 04 '22 at 16:41
  • @BenoîtFraikin The question as asked is very explicitly not (only) about the monad transformer, but also about the monad it produces: "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.". This quote asks about the `Monad` instance, not the `MonadTrans` instance. `lift`'s behavior alone is not enough to know about the `Monad` behavior. – Daniel Wagner Jun 04 '22 at 22:42
0

The identity monad has at least two monad transformers: the identity monad transformer and the codensity monad transformer.

newtype IdentityT m a = IdentityT (m a)
newtype Codensity m a = Codensity (forall r. (a -> m r) -> m r)

Indeed, considering Codensity Identity, forall r. (a -> r) -> r is isomorphic to a.

These monad transformers are quite different. One example is that "bracket" can be defined as a monadic action in Codensity:

bracket :: Monad m => m () -> m () -> Codensity m ()
bracket before after = Codensity (\k -> before *> k () *> after)

whereas transposing that signature to IdentityT doesn't make much sense

bracket :: Monad m => m () -> m () -> IdentityT m ()  -- cannot implement the same functionality

Other examples can be found similarly from variants of the continuation/codensity monad, though I don't see a general scheme yet.

The state monad corresponds to the state monad transformer and to the composition of Codensity and ReaderT:

newtype StateT s m a = StateT (s -> m (s, a))
newtype CStateT s m a = CStateT (Codensity (ReaderT s m) a)

The list monad corresponds to at least three monad transformers, not including the wrong one:

newtype ListT m a = ListT (m (Maybe (a, ListT m a)))  -- list-t
newtype LogicT m a = LogicT (forall r. (a -> m r -> m r) -> m r -> m r)  -- logict
newtype MContT m a = MContT (forall r. Monoid r => (a -> m r) -> m r))

The first two can be found respectively in the packages list-t (also in an equivalent form in pipes), and logict.

Li-yao Xia
  • 27,891
  • 2
  • 29
  • 51