Monad Laws for applicative wording

Question

Usually in Haskell we define Monad 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 quite intuitive once you get used to them.

There is another way to define monads in terms of the Applicative functor:

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

I am interested in laws for this kind of language. Obviously, we could simply adapt the fmap + join laws as follows (I'm not sure if the names are particularly relevant, but good):

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

Obviously, these conditions are enough for pure , (<*>) and myJoin to form a monad (in the sense that they guarantee that m `myBind` f = myJoin (pure f <*> m) will behave well >>= ). But are they also needed? It seems that the additional structure supported by Applicative above and above Functor can allow us to simplify these laws - in other words, that some functions from the above laws can be specified that it is known that pure and (<*>) already satisfy Applicative laws.

(In case you are wondering why we even bothered to worry about this wording, given one of two standard features: I'm not sure if all this is useful or insightful in the programming context, but it turns out if you use Monad to make the natural semantics of langauge .)

Answer 1

The law of identity is much easier to write down

 join . fmap pure = join . pure = id 

The traditional law of the right to monads immediately follows from the definition >>= . Law of Left Identity Uses Applicative Law

 m >>= k = join (fmap km) -- 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 = fa join (fmap f (pure a)) = fa -- definitions of >>= and return join (pure (fa)) = fa -- fmap f . pure = pure . f id (fa) = fa -- identity fa = fa -- definition of id 

An interesting law for the 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

 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 may be a more elegant way to write this.

I have not found a way to show that Monad associative based

• Functor and Applicative laws, in particular the composition <*>
• Identities join . fmap pure = join . pure = id join . fmap pure = join . pure = id
• (<*>) = ap

and I'm not sure if this is true. I think you need an associative join . join = join . fmap join law join . join = join . fmap join join . join = join . fmap join