13

While I was learning Composing Types chapter from Haskell Book, I was given tasks to write Functor and Applicative instances for the following type.

newtype Compose f g a = Compose { getCompose :: f (g a) }

I wrote the following definitions

Functor:

fmap f (Compose fga) = Compose $ (fmap . fmap) f fga

Applicative:

(Compose f) <*> (Compose a) = Compose $ (<*>) <$> f <*> a

I learned that composing two Functors or Applicatives gives Functor and Applicative respectively.

The author also explained it is not possible to compose two Monads the same way. So we use Monad Transformers. I just do not want to read Monad Transformers unless I'm clear with why Monads do not compose.

So far I tried to write bind function like this:

Monad:

(>>=) :: Compose f g a -> (a -> Compose f g b) -> Compose f g b
(Compose fga) >>= h = (fmap.fmap) h fga

and of course got this error from GHC

Expected type: Compose f g b

Actual type: f (g (Compose f g b))

If I can strip the outermost f g somehow, the composition gives us a monad right? (I still couldn't figure out how to strip that though)

I tried reading answers from other Stack Overflow questions like this, but all answers are more theoretical or some Math. I still haven't learned why Monads do not compose. Can somebody explain me without using Math?

Community
  • 1
  • 1
  • 2
    @RobinZigmond But given that a monad is a functor, *something* about the extra structure in a monad "breaks" composition. I think that's what the OP is looking for, what that "something" is. – chepner Mar 07 '19 at 13:48
  • @NirvinM - not sure why you think I'm being "mean". I'm just trying to understand what you need by way of further explanation. (Not that I'm necessarily able to give it, being no expert in this area.) @chepner - I agree, unfortunately I had to drastically cut my original comment due to the character limit so the part where I acknowledged that ended up not being there. But I think the linked-to answer did a good job about explaining that, based on the `join` definition of a Monad (I presume something similar happens when you try using `>>=`) – Robin Zigmond Mar 07 '19 at 13:51
  • @RobinZigmond Perhaps what's missing form the linked answer is a concrete counterexample. The answer simply shows that if we attempt to prove that monads compose in the straightforward way, we fail. Strictly speaking, this does not prove that monads don't compose: we need a counterexample. – chi Mar 07 '19 at 14:10
  • Note that even though monads are not closed under composition, monad transformers are indeed closed under composition. Though it won't work with the kind of composition you have in your example, you need one which works for higher kinds. – svenningsson Mar 07 '19 at 14:52
  • Does this answer your question? https://stackoverflow.com/questions/7040844/applicatives-compose-monads-dont – Benjamin Hodgson Mar 07 '19 at 16:24

1 Answers1

18

I think this is easiest to understand by looking at the join operator:

join :: Monad m => m (m a) -> m a

join is an alternative to >>= for defining a Monad, and is a little easier to reason about. (But now you have an exercise to do: show how to implement >>= from join, and how to implement join from >>=!)

Let's try to make a join operation for Composed f g and see what goes wrong. Our input is essentially a value of type f (g (f (g a))), and we want to produce a value of type f (g a). We also know that we have join for f and g individually, so if we could get a value of type f (f (g (g a))), then we could hit it with fmap join . join to get the f (g a) we wanted.

Now, f (f (g (g a))) isn't so far from f (g (f (g a))). All we really need is a function like this: distribute :: g (f a) -> f (g a). Then we could implement join like this:

join = Compose . fmap join . join . fmap (distribute . fmap getCompose) . getCompose

Note: there are some laws that we would want distribute to satisfy, in order to make sure that the join we get here is lawful.

Ok, so that shows how we can compose two monads if we have a distributive law distribute :: (Monad f, Monad g) => g (f a) -> f (g a). Now, it could be true that every pair of monads has a distributive law. Maybe we just have to think really hard about how to write one down?

Unfortunately there are pairs of monads that don't have a distributive law. So we can answer your original question by producing two monads that definitely don't have a way of turning a g (f a) into an f (g a). These two monads will witness to the fact that monads don't compose in general.

I claim that g = IO and f = Maybe do not have a distributive law

-- Impossible!
distribute :: IO (Maybe a) -> Maybe (IO a)

Let's think about why such a thing should be impossible. The input to this function is an IO action that goes out into the real world and eventually produces Nothing or a Just x. The output of this function is either Nothing, or Just an IO action that, when run, eventually produces x. To produce the Maybe (IO a), we would have to peek into the future and predict what the IO (Maybe a) action is going to do!

In summary:

  • Monads can compose if there is a distributive law g (f a) -> f (g a). (but see the addendum below)
  • There are some monads that don't have such a distributive law.
  • Some monads can compose with each other, but not every pair of monads can compose.

Addendum: "if", but what about "only if"? If all three of F, G, and FG are monads, then you can construct a natural transformation δ : ∀X. GFX -> FGX as the composition of GFη_X : GFX -> GFGX followed by η_{GFGX} : GFGX -> FGFGX and then by μ_X : FGFGX -> FGX. In Haskellese (with explicit type applications for clarity), that would be

delta :: forall f g x. (Monad f, Monad g, Monad (Compose f g))
      => g (f x) -> f (g x)
delta = join' . pure @f . fmap @g (fmap @f (pure @g)) 
  where
    -- join for (f . g), via the `Monad (Compose f g)` instance
    join' :: f (g (f (g x))) -> f (g x)
    join' = getCompose . join @(Compose f g) . fmap Compose . Compose

So if the composition FG is a monad, then you can get a natural transformation with the right shape to be a distributive law. However, there are some extra constraints that fall out of making sure your distributive law satisfies the correct properties, vaguely alluded to above. As always, the n-Category Cafe has the gory details.

Matt Noonan
  • 296
  • 2
  • 5
  • distribute aka sequenceA? the types fit (besides the Traversable constraint on `g`) – Will Ness Mar 07 '19 at 15:53
  • @WillNess there are various way to distribute functors, e.g. http://hackage.haskell.org/package/distributive-0.6/docs/Data-Distributive.html is another one. – phadej Mar 07 '19 at 16:08
  • while this is a good answer, I'm not sure the counterexample is totally convincing given that `unsafePerformIO` exists, which should be "impossible" for much the same reason. – Robin Zigmond Mar 07 '19 at 16:28
  • @RobinZigmond: I think there are two answers to that: (1) We reason about `Monad` in the total and pure fragment of Haskell – if we don't worry about `undefined`, we certainly don't worry about `unsafePerformIO` (especially since `unsafePerformIO` can be used to implement `unsafeCast :: a -> b`). (2) `unsafePerformIO` doesn't (I presume) satisfy the laws that, as Matt mentioned, we need for the resulting `Monad` instance to be lawful. – Antal Spector-Zabusky Mar 07 '19 at 18:12
  • I take your point, that `unsafePerformIO` is exceptional, because it isn't a pure function. But `IO` still satisfies the Monad laws - `unsafePerformIO` doesn't change that at all. Of course if we disallow impure functions then there can be no function `IO (Maybe a) -> Maybe (IO a)` (because there can be no function `IO a -> b` unless `b = IO c` for some `c`). But this still raises the question of whether it is only in the pure subset of Haskell that Monads fail to be closed under composition, or whether there's some deeper explanation than the need for purity. I don't know the answer to that! – Robin Zigmond Mar 07 '19 at 18:39
  • 3
    @RobinZigmond `distribute ( getLine >>= (\s -> if length s > 2 then return (Just s) else return Nothing) ) :: Maybe (IO String)`. So it's a value which **already knows** what a user **will type**. If it's `Just act`, we can execute that `act`, and it will magically produce a user which is guaranteed to type in no less than 3 characters! that's not unsafe I/O, that's pure magic. // that's how I understand that argument anyway. – Will Ness Mar 07 '19 at 18:48
  • @RobinZigmond I saw your thanks, and you're welcome. :) wanted to write a longer reply, got distracted -- something about timelines and how this flipping of monads' order is similar to having the "`runMonad`" function which we don't have for the IO in the "now", since it runs strictly in "the future". something like that. – Will Ness Mar 08 '19 at 09:30
  • Thanks. That explains why the composition should'nt be possible. Is it that the Type System smart enough to prevent this kind of definition or just a coincidence? –  Mar 08 '19 at 10:32
  • A counterexample with a different accent: `Const ()` and `Const Void` (in the total fragment) surely do not distribute. – luqui Mar 08 '19 at 18:30
  • I think you may want to explain a bit more the **only** in "Monads can only compose if ...". You argue that monads can compose if we have a distribute, but it's not clear to me why your argument would show that monads can only compose if we have a distribute. – dvitek Jan 03 '21 at 15:46
  • @dvitek oof, yes, that was sloppy. The "only" is slightly subtle: you can construct a natural transformation with the right type to be a distributive law, but you need a bit more in order to get it to satisfy the correct properties. I've added some of the details to the answer. – Matt Noonan Jan 04 '21 at 05:02
  • @MattNoonan OK, thanks for clarifying! That looks roughly like what I had in mind, although your reference to the nLab and the details there about certain compositions being the right things are points I definitely would have overlooked. – dvitek Jan 04 '21 at 22:59
  • The State monad doesn't have a distributive law with any other monad. No need to use IO to get that example. – winitzki Dec 05 '22 at 20:29