Monad, Applicative, Functor: Add equations for default definitions and superclass methods

[HeinrichApfelmus]

When working with the Monad, Applicative and Functor classes, I found some room for improvement.

Specifically, I have formalized a proof that the Monad laws imply the Applicative laws which I would like to backport to base.agda-lib.

Currently, the Monad class is split into the full class, and the default implementation for some methods:

  record Monad (m : Type → Type) : Type₁ where
    field
      _>>=_ : m a → (a → m b) → m b
      overlap ⦃ super ⦄ : Applicative m
      return : a → m a
      _>>_ : m a → (@0 {{ a }} → m b) → m b
  -- ** defaults
  record DefaultMonad (m : Type → Type) : Type₁ where
    field
      _>>=_ : m a → (a → m b) → m b
      overlap ⦃ super ⦄ : Applicative m
    return : a → m a
    return = pure

    _>>_ : m a → (@0 {{ a }} → m b) → m b
    m >> m₁ = m >>= λ x → m₁ {{x}}

I would like to argue that:

1. The class Monad should include equations for all default methods, such as

     prop->>->>=
       : ∀ ⦃ _ : Monad m ⦄ ⦃ _ : IsLawfulMonad m ⦄
       → (mx : m a) (my : @0 ⦃ a ⦄ → m b)
       → mx >> my  ≡  mx >>= (λ x → my ⦃ x ⦄)

   In other words, we can rely on the fact that (>>) is propositionally equal to its default definition, we just cannot assume that this equality holds by computation.

   I think it's fair to put these equalities in the Monad class as opposed to the IsLawfulMonad class, because these are about default definitions of functions, not about properties that these functions should have.

   By the way, as far as I can tell, with the current setup of IsLawfulMonad, I don't think that it's possible to prove prop->>->>= — I had to postulate it. :O

2. Similarly, the class Monad should include equations for all methods from superclasses, such as the definition of fmap in terms of >>= and return:

     prop-fmap->>=
       : ∀ {a b} (f : a → b) (ma : m a)
       → fmap f ma ≡ (ma >>= (return ∘ f))    

   Again, this argument is about the expected default definitions of functions. This particular property is currently part of IsLawfulMonad, but I'm arguing that it should be part of Monad directly.

3. As an exceptional addition to 2., I would like to make the equality return ≡ pure computational, because this case is very common and also because there is a trend in Haskell to move return out of fashion and use pure instead.

(4. In Haskell, it is common to associate type classes with laws. Thus, I also think that merging the Monad and the IsLawfulMonad type classes is sensible. However, this argument is left for the future, I do not want to make it for this issue.)

What do you think?

I'm happy to contribute relevant code. In particular, I would like to backport the proof that the Monad laws imply the Applicative laws — this will require talking about a version of the Monad laws that does not already presume the Applicative laws. Adding the default definitions as equalities to the type classes are a first step in that direction.

[omelkonian]

Totally agree on the motivation and suggested solution; please open a PR with the most uncontroversial of these laws (e.g. the Monad/Applicative interface laws will do), so that we can flesh out the details and then merging other instances will be straightforward.