Monad more powerful than Applicative?

Question

I looked at past discussion but could not see why any of the answers are actually correct.

Applicative

<*> :: f (a -> b) -> f a -> f b

Monad

(>>=) :: m a -> (a -> m b) -> m b

So if I get it right, the claim is that >>= cannot be written by only assuming the existence of <*>

Well, let's assume I have <*>.

And I want to create >>=.

So I have f a.

I have f (a -> b).

Now when you look at it, f (a -> b) can be written as (a -> b) (if something is a function of x, y , z - then it's also a function of x, y).

So from the existence of <*> we get (a -> b) -> f a -> f b which again can be written as ((a -> b) -> f a) -> f b, which can be written as (a -> f b).

So we have f a, we have (a -> f b), and we know that <*> results in f b, so we get:

f a -> (a -> f b) -> f b

which is a monad.

Actually, in a more intuitive language: when implementing <*>, I extract (a -> b) out of f(a -> b), I extract a out of f a, and then I apply (a -> b) on a and get b which I wrap with f to finally get f b.

So I do almost the same to create >>=. After applying (a -> b) on a and getting b, do one more step and wrap it with f, so I return f b, hence I know I have a function (a -> f b).

Answer 1

Now when you look at it, f(a -> b) can be written as (a -> b)

No. It can't. Your intuition is (dangerously) far off at this point. That's like saying a hammer is perfect for driving screws in, since it already works for a nail*. You can't simply drop f here, it's part of the type**.

Instead, let's get the facts straight. An Applicative has three associated functions, counting Functor's fmap:

fmap  :: Functor f     =>   (a -> b) -> f a -> f b
pure  :: Applicative f =>                 a -> f a
(<*>) :: Applicative f => f (a -> b) -> f a -> f b

Here's another fact: you can define bind ((>>=)) in terms of join and vice versa:

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

(>>=) :: Monad m => m a -> (a -> m b) -> m b
k >>= f = join (fmap f k)

are the implementations of join and bind you provided here part of the Monad definition, or are only join and bind signatures part of the Monad definition? [...] So now I ask myself why would they bother.

Those aren't the official definitions of course, since they would never terminate. You have to define (>>=) for your type if you want to make it a a monad:

instance Monad YourType where
   k >>= f = ...

Also, your join definition uses id which is not in the Monad interface, why is it mathematically legitimate?

First of all, id :: a -> a is defined for any type. Second, the mathematical definition of a monad is actually via join. So it's "more"*** legitimate. But most important of all, we can define the monad laws in terms of join (exercise).

If we created join via Applicative, we could also create bind. If we cannot create join via Applicative methods, neither can we derive bind. And join's type actually makes it obvious that we cannot derive it from Applicative:

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

Join is able to drop one of the m layers. Let's check whether it's possible to do the same in the other methods:

fmap  :: Functor f     =>   (a -> b) -> f a -> f b
                          ^                    ^
                        0 here              1 here

pure  :: Applicative f =>                 a -> f a
                                          ^  | ^
                                      0 here | 1 here

(<*>) :: Applicative f => f (a -> b) -> f a -> f b
                          ^                    ^
                       1 here                1 here

The answer is no: none of the tools we're given by Applicative enables us collapse multiple m's into a single one. And that's also what is written in the Typeclassopedia right after the cited paragraph in the other question:

To see the increased power of Monad from a different point of view, let’s see what happens if we try to implement (>>=) in terms of fmap, pure, and (<*>). We are given a value x of type m a, and a function k of type a -> m b, so the only thing we can do is apply k to x. We can’t apply it directly, of course; we have to use fmap to lift it over the m. But what is the type of fmap k? Well, it’s m a -> m (m b). So after we apply it to x, we are left with something of type m (m b)—but now we are stuck; what we really want is an m b, but there’s no way to get there from here. We can add m’s using pure, but we have no way to collapse multiple m’s into one.

Note that join doesn't make it possible to get rid of m completely, that would be a total extraction, and—depending on some other functions—a feature of a comonad. Either way, make sure that you don't let your intuition go astray; trust and use the types.

_{* That comparison is a little bit bad, because you could actually try to dive a screw in with a hammer into a piece of wood. So think of a plastic screw, a rubber hammer and a carbon steel plate you want to drive the nail in. Good luck.}

_{** Well, you can drop it, but then the type changes drastically.}

_{*** Given that (>>=) and join are equivalent of power and any (>>=) using formula can be transformed to one only using join, they are of course both mathematical sound.}

Answer 2

Now when you look at it, f (a -> b) can be written as (a -> b)

Everyone has already contributed explaining that this is not a fact. Let me prove it to you.

If we genuinely had what you state then we should be able to write a function

expose :: f (a -> b) -> (a -> b)

Moreover, for any concrete data type we like, call it F, we ought to be able to write

expose_F :: F (a -> b) -> (a -> b)
expose_F = expose

Let's worry only about writing expose_F since if we can show that expose_F cannot be written for some F then we have surely shown that expose cannot be written.

---

Let me provide us a test F. It will certainly be non-intuitive feeling as I'm intending to use it to break intuition, but I'm happy to confirm all day long that there is nothing funny at all about

data F a = F

Indeed, it is a Functor

instance Functor F where
  fmap _ F = F

and an Applicative for that matter

instance Applicative F where
  pure _ = F
  F <*> F = F

even a Monad

instance Monad F where
  return _ = F
  F >>= _ = F

You can verify yourself that all of these typecheck. There's nothing wrong at all about F.

So what's just right about, F? Why did I choose it? Well F is interesting in that values of F a fail to contain anything related at all to a within them. Often people like to talk about data types (or Functors) as "containers" or "boxes". F forces us to remember that in a certain sense a box that's 0 inches deep is still a box. [0]

So surely we cannot write

expose_F :: F (a -> b) -> (a -> b)

---

There are a number of ways of proving this. The easiest is to appeal to my supposition that you, for instance, believe that there is no coerce function. But, if we had expose_F there would be!

coerce :: a -> b
coerce = expose_F F

More specifically, let me introduce another pathological type (which I again assure you is totally fine)

data Void

There are zero constructors of Void and we like to say therefore that Void has no members. It cannot be made to exist. But we can make one with expose_F.

void :: Void
void = expose_F F ()

In Haskell we're not technically sound enough to execute the above proofs. If you dislike the way I talk about impossibility then you can conjure up whatever types you like with a convenient infinite loop, casual call to

 error "Madness rides the star-wind... claws and teeth sharpened on centuries of corpses... dripping death astride a bacchanale of bats from nigh-black ruins of buried temples of Belial..."

or perhaps an unassuming undefined. But these are all on the path of madness.

---

There is no expose_F and therefore there is no expose.

---

[0] And to be completely clear, thinking of data types as boxes at all is often flawed. Instances of Functor tend to be "box-like", but here's another interesting data type which is difficult to think of as a box

data Unbox a = Unbox (a -> Bool)

unless perhaps you consider Unbox a to be a box containing a Bool and a negative a or something like that. Perhaps an IOU a.