Monad laws for an applicative-based formulation

Question

Normally in Haskell we define Monads in terms of return and >>=. Sometimes it's convenient to decompose >>= into fmap and join. The Monad laws for these two formulations are well known and fairly intuitive, once you get used to them.

There's another way to define monads, in terms of an Applicative functor:

class Applicative f => MyMonad f where
    myJoin :: f (f a) -> f a

I'm wondering about the laws for this kind of formulation. Obviously, we could just adapt the fmap + join laws, as follows (I am not sure the names are particularly apt, but oh well):

myJoin . myJoin = myJoin . (pure myJoin <*>)       ('Associativity')
myJoin . pure   = myJoin . (pure pure   <*>) = id  ('Identity')

Clearly these conditions are sufficient for pure, (<*>), and myJoin to form a monad (in the sense that they guarantee that m `myBind` f = myJoin (pure f <*> m) will be a well-behaved >>=). But are they necessary as well? It seems at least possible that the additional structure that Applicative supports above and beyond Functor might allow us to simplify these laws -- in other words, that some feature of the above laws might be otiose given that it is known that pure and (<*>) already satisfy the Applicative laws.

(In case you're wondering why we'd even go to the trouble of bothering with this formulation given either of the two standard possibilities: I'm not sure it's all that useful or perspicuous in programming contexts, but it turns out to be so when you use Monads to do natural langauge semantics.)

Answer 1

The identity law is much easier to write

join . fmap pure = join . pure = id

The traditional monad right identity law follows immediately from the definition of >>=. The left identity law uses an Applicative law

m >>= k = join (fmap k m)

-- proof for right identity
m >>= return       = m
join (fmap pure m) = m  -- definition of >>=
id m               = m  -- identity
m                  = m  -- definition of id

-- proof for left identity
return a >>= f         = f a
join (fmap f (pure a)) = f a  -- definitions of >>= and return
join (pure (f a))      = f a  -- fmap f . pure = pure . f
id (f a)               = f a  -- identity
f a                    = f a  -- definition of id

The interesting law for a relationship between Applicative and Monad is

(<*>) = ap
-- or
m1 <*> m2 = m1 >>= (\x1 -> m2 >>= \x2 -> return (x1 x2)) -- definition of ap

In terms of Applicative and join this is

m1 <*> m2 = join (fmap (\x1 -> fmap x1 m2) m1)
-- proof
m1 <*> m2 = join (fmap (\x1 -> m2 >>= \x2 -> return (x1 x2)) m1)            -- definition of ap
m1 <*> m2 = join (fmap (\x1 -> join (fmap (\x2 -> return (x1 x2)) m2)) m1)  -- definition of >>=
m1 <*> m2 = join (fmap (\x1 -> join (fmap (\x2 -> pure (x1 x2)) m2)) m1)    -- return = pure
m1 <*> m2 = join (fmap (\x1 -> join (fmap (pure . x1) m2)) m1)                 
m1 <*> m2 = join (fmap (\x1 -> join (fmap pure (fmap x1 m2))) m1)           -- fmap (f . g) = fmap f . fmap g
m1 <*> m2 = join (fmap (\x1 -> fmap x1 m2) m1)                              -- identity

There might be a more elegant way to write this.

I haven't found a way to show that the Monad is associative based on

• Functor and Applicative laws - particularly composition of <*>
• The identities join . fmap pure = join . pure = id
• (<*>) = ap

and I'm not sure if it's true. I think you need the associative law join . join = join . fmap join