4

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
  • 148
  • 9
  • 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
  • @DanielWagner Do you mean that one would give two separate `instance` declarations for `T Identity` and `T []`? Of course then (if that's what you meant) one could define each however one wishes. However, that feels more like two separate transformers than one transformer (as an alternative to MaybeT). I think what would be sufficient for a "non-degenerate" case is for the transformer to have one declaration of the form `instance (Monad m) => Monad (T m) where`. Not sure if this is asking too much. I have so far only skimmed the answers but I think I'll be wiser after reading them with care. – QuantumWiz Jun 06 '22 at 00:08
  • @QuantumWiz With the technique I'm thinking of (GADTs), it would be possible to write just a single instance. – Daniel Wagner Jun 06 '22 at 01:02

3 Answers3

3

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
  • 145,880
  • 9
  • 220
  • 380
  • 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
  • What's the definition of `return`? Is it `Twice . return . return` or did I misunderstand? – QuantumWiz Jun 06 '22 at 09:14
  • @QuantumWiz You understood. – Daniel Wagner Jun 06 '22 at 14:40
  • @DanielWagner Sorry for the late comment but I wanted to thank you. Your answer and that of Li-yao Xia complement each other nicely. Yours is easy to understand, at least on conceptual level, though it's slightly artificial and limited to monads with `swap`. Li-yao Xia's answer doesn't have that restriction and is seemingly a "real" example. However, it's much more difficult to understand than your answer. I wish I could accept both of your answers. – QuantumWiz Jun 23 '22 at 12:38
  • @DanielWagner I tried to figure out what `(>>=)` would be if I don't directly use your `join` but still base it on it. I got `x >>= f = Twice $ fmap join $ join $ fmap swap $ fmap (fmap f) $ runTwice $ x`. Is this correct or did I make a mistake? – QuantumWiz Jun 23 '22 at 13:52
  • @QuantumWiz I guess you've missed a newtype unwrapping (`fmap (fmap (runTwice . f))` instead of `fmap (fmap f)`). Otherwise that looks right to me. – Daniel Wagner Jun 23 '22 at 17:53
  • `Twice` is not a correct monad transformer because `Twice` cannot be applied to an arbitrary monad `m`, only to certain monads that have `swap`. A monad transformer `t` should produce a new lawful monad `t m` for any monad `m`, not just for a subset of monads. – winitzki Oct 01 '22 at 16:49
1

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
  • 31,896
  • 2
  • 33
  • 56
  • Do I understand correctly that `Codensity` is both a monad transformer and also a monad in the sense that it doesn't have to be applied to another monad to be an instance of `Monad`? – QuantumWiz Jun 13 '22 at 15:01
  • No it's only a monad transformer. – Li-yao Xia Jun 13 '22 at 18:48
  • But the instance declaration is just `instance Monad (Codensity f) where` (or in newer GHC versions `instance Monad (Codensity (f :: k -> TYPE rep)) where`). There doesn't seem to be a restriction that f would have to be a monad. For comparison, e.g. the monad instance declaration for `MaybeT` is `instance (Monad m) => Monad (MaybeT m) where` so it's a requirement that m is a monad. – QuantumWiz Jun 13 '22 at 21:54
  • Ah in *that* sense, yes, it's more general than a monad transformer. I thought you meant `Monad Codensity` which isn't well-typed. – Li-yao Xia Jun 13 '22 at 22:21
  • Your answer is pretty good because it's an example which is (presumably) actually in use rather than just an artificial counterexample. However, I'm struggling to understand what Codensity does. Is there a short intuitive explanation? – QuantumWiz Jun 14 '22 at 09:46
  • 1
    Codensity is to monads as [difference lists](https://hackage.haskell.org/package/dlist) are to lists. See also [Notions of computation as monoids](https://arxiv.org/abs/1406.4823). – Li-yao Xia Jun 14 '22 at 13:04
  • @Li-yaoXia What about the type `newtype LT m a = LT (forall r. (a -> m (r -> r)) -> m (r -> r))`? Is this yet another transformer for the `List` monad? This is a more straightforward application of the codensity monad's transformer. – winitzki Dec 09 '22 at 10:51
  • Yeah, that's another example. It looks quite close to `MContT`, since the only thing you can do with `(r -> r)` functions is to compose them or form the identity. – Li-yao Xia Dec 09 '22 at 11:05
1

There is another example of a monad that has two inequivalent transformers: the "selection" monad.

 type Sel r a = (a -> r) -> a

The monad is not well known but there are papers that mention it. Here is a package that refers to some papers:

https://hackage.haskell.org/package/transformers-0.6.0.4/docs/Control-Monad-Trans-Select.html

That package implements one transformer:

type SelT r m a = (a -> m r) -> m a

But there exists a second transformer:

type Sel2T r m a = (m a -> r ) -> m a

Proving laws for this transformer is more difficult but I have done it.

An advantage of the second transformer is that it is covariant in m, so the hoist function can be defined:

 hoist :: (m a -> n a) -> Sel2T r m a -> Sel2T r n a

The second transformer is "fully featured", has all lifts and "hoist". The first transformer is not fully featured; for example, you cannot define blift :: Sel r a -> SelT r m a. In other words, you cannot embed monadic computations from Sel into SelT, just like you can't do that with the Continuation monad and the Codensity monad.

But with the Sel2T transformer, all lifts exist and you can embed Sel computations into Sel2T.

This example shows a monad with two transformers without using the Codensity construction in any way.

winitzki
  • 3,179
  • 24
  • 32