Reorganize Monad laws, prove Applicative laws

[HeinrichApfelmus]

This pull request reorganizes the IsLawfulMonad class.

The main reason for this reorganization is that IsLawfulFunctor and IsLawfulApplicative are actually consequences of MonadLaws and IsDefaultMonad. However, this fact is difficult to use in the old definition as the other two classes are used as superclasses.

Context: #411

Comments

While not in the scope of this pull request, possible future reorganizations are:

1. Drop the IsLawfulApplicative superclass from IsLawfulMonad and make it a global consequence instead, i.e. add a global instance _ : {{IsLawfulMonad m}} → IsLawfulApplicative m.

   This has the slight drawback that the existing instance of IsLawfulApplicative need to be removed while making sure that Haskell.Law.Applicative re-exports the global instance. Then again, the IsLawfulMonad instance is the easiest way to prove IsLawfulApplicative, and in the spirit of proof-irrelevance, we don't actually care how we have proven IsLawfulMonad.

2. Merge the IsDefaultMonad class into the Monad class.

   Reason: In Haskell, it is traditional to expect the Monad constraint to imply the laws mentioned in the documentation. For usage sites, this means that Monad is sufficient, the IsLawfulMonad constraint is conceptually implied by the Monad class. This conceptual model works until we actually have to formalize proofs, at which point we want to develop proofs incrementally. For incremental development of proofs, the separation between "implementation" (Monad) and "properties" (IsLawfulMonad) is very useful, but I would argue that this case rarely happens specifically for the Monad class, where instances are seldomly defined by library users. (In contrast, Eq and Ord are frequently defined by library users for their own data types, and the separation of IsLawfulEq and IsLawfulOrd is more valueable.)

   As a first step towards conceptual unification, I would propose to merge IsDefaultMonad into the Monad class, as the equality to the default implementations is uncontroversial.

3. Merge the IsLawfulMonad class into the Monad class. Same reasoning as in 2., but more extreme.

[jespercockx]

Thanks for the PR!

Regarding incremental development: ideally there should be a gradual path:

1. An implementation without any specification.
2. An implementation that states its specification but doesn't prove it.
3. An implementation together with a specification and a proof.

The current design allows all three: one can just implement a Monad instance at first, then later add a postulate that it is lawful (which can already be used in other proofs that use the monad) and finally replace the postulate with an actual proof. If we merge IsLawfulMonad into the Monad class then it is no longer possible to have just an implementation of the monad interface without making any claims about its behavior.

Another argument against merging the laws into the class is that sometimes, Haskell programmers actually do implement non-lawful monads, and then it would be inconsistent to postulate that such a monad is lawful.

[HeinrichApfelmus]

If we merge IsLawfulMonad into the Monad class then it is no longer possible to have just an implementation of the monad interface without making any claims about its behavior.

Yes, though the argument about making these postulates would equally apply to this situation.

Another argument against merging the laws into the class is that sometimes, Haskell programmers actually do implement non-lawful monads, and then it would be inconsistent to postulate that such a monad is lawful.

That is true, but specifically for Monad, such implementations are generally frowned upon — with one notable exception: When the Monad preserves an equivalence relation ~, but not propositional equality ≡. Unfortunately, this situation arises frequently for free monads. (At some point, we will need quotient types. The problem applies to IsLawfulEq as well, by the way.)

Just for the record: The benefit of merging the two classes would be that any general proposition about monads has a shorter type, because it only needs to mention ⦃ _ : Monad m ⦄ as an argument, as opposed to the longer ⦃ _ : Monad m ⦄ ⦃ _ : IsLawfulMonad m ⦄.

[jespercockx]

It should be possible to add quotient types (with postulates + perhaps a rewrite rule) so I'd say that's not a showstopper for this PR. But since it's not really connected to this issue, please make a separate issue for that.

I do agree that not needing a separate constraint for the laws is nice. But this could in principle also be achieved by defining a bundled class LawfulMonad that contains both a monad and its IsLawful proof (and has eta-equality).

[omelkonian]

Looks good overall, I've just pointed some design changes to make the approach more maintanable.

[omelkonian]

While I agree with the MonadLaws/IsLawfulMonad separation, I don't think we should also separate IsDefaultMonad/MonadLaws; one only has the monad laws proven when the user's instance has implemented correctly the default fields.

[HeinrichApfelmus]

The nomenclature "monad laws" typically refers to the three identities I originally put in the record MonadLaws — and only those three identities.

For example, Hutton, "Programming in Haskell", (2018), p. 174 writes:

Monad laws

In a similar manner to functors and applicatives, the two monadic primitives are required to satisfy some equational laws:

return x >>= f    =  f x
mx >>= return     =  mx
(mx >>= f) >>= g  =  mx >>= (\ x -> (f x >>= g))

The identities that I had put in the IsDefaultMonad record concern the definition of functions that are traditional or relate to superclasses, but are not part of the "monad laws", such as pure, >>, fmap, and (<*>).

In other words, in principle, it is possible for a user instance of Monad to implement the "monad laws" correctly while implementing the traditional and superclass functions incorrectly.

(The documentation for Control.Monad in the base package tries to help by listing (a subset of) relevant laws, but it's not an authoritative list of the "monad laws".)

In that light, I figured that it would make sense for me to mirror the conceptual grouping of laws with two explicit records. This has the additional benefit that I can ask the question whether IsDefaultMonad should be merged with the Monad class, while keeping MonadLaws separate. The idea is that IsDefaultMonad concerns the definitions of certain functions, while MonadLaws concerns properties that do not have the form of a definition.

(I want to note that using this conceptual grouping makes it easier to ask the question of "Is there a law for each function definition?", which in turn makes it possible to discover that def->>->>= is not provable from the implementation before this pull request.)

That said, I don't mind lumping MonadLaws and IsDefaultMonad together — this would reflect a different conceptual grouping along the lines of "function definitions" (Monad) and "any properties those functions may have" (MonadLaws).

[omelkonian]

The identities that I had put in the IsDefaultMonad record concern the definition of functions that are traditional or relate to superclasses, but are not part of the "monad laws", such as pure, >>, fmap, and (<*>).

Then it's the wrong name :P

That said, I don't mind lumping MonadLaws and IsDefaultMonad together

Just to be clear, I'm not suggesting a single record with all laws, we've confused two separate orthogonal issues:

1. separating the laws about default methods in IsDefaultMonad
2. separating the monad laws into the "pure" Monad laws and interactions with superclasses

I completely agree with (1), but done in a DRY fashion.
I don't have a strong opinion for (2), but it can wait for a future PR when the separation has at least a single use.

[omelkonian]

I'd like to think of default methods and superclasses as completely separate issues/laws.

These can still remain in their original place in MonadLaws, right?

[HeinrichApfelmus]

(See my other comment #412 (comment) . In short, the definitions of superclass methods are not part of the nomenclature of the three "monad laws", hence me grouping them with the other definition-like properties.)

[omelkonian]

Still doesn't make sense to have monad-functor laws inside the IsDefaultMonad.

[omelkonian]

Too wordy and a bit confusing. If you apply my suggested refactoring, rephrase as:

-- Monad laws
--
-- Note that `MonadLaws` do not yet require that the superclasses are themselves lawful; this is deferred to `IsLawfulMonad` as these can sometimes be proven via the `MonadLaws`.

(the comment about superclass instances in scope is irrelevant)

[HeinrichApfelmus]

I have changed the comment on PreLawfulMonad in the manner you suggested.

That done, I do think that the only difference between PreLawfulMonad and IsLawfulMonad is the scope of IsLawfulApplicative and IsLawfulFunctor, because we have proofs prop-PreLawfulMonad→IsLawfulApplicative and prop-PreLawfulMonad→IsLawfulFunctor.

[omelkonian]

I agree with @jespercockx in keeping Monad and IsLawfulMonad separate.

HEINRICH: Just for the record: The benefit of merging the two classes would be that any general proposition about monads has a shorter type, because it only needs to mention ⦃ _ : Monad m ⦄ as an argument, as opposed to the longer ⦃ _ : Monad m ⦄ ⦃ _ : IsLawfulMonad m ⦄.
JESPER: I do agree that not needing a separate constraint for the laws is nice. But this could in principle also be achieved by defining a bundled class LawfulMonad that contains both a monad and its IsLawful proof (and has eta-equality).

Yep, that's not a valid argument for merging. One could also make this construction more generic so that it works for any "typeclass conjuction" (although it breaks once you move to higher universe levels..., but since we only use Types at level 0 we should be fine here).

[jespercockx]

@HeinrichApfelmus I see you pushed some changes here, could you please give a summary of the status of this PR? Are there any remaining questions to be addressed?

[HeinrichApfelmus]

I see you pushed some changes here, could you please give a summary of the status of this PR? Are there any remaining questions to be addressed?

The status of this PR is "blocked due to disagreement". 😅

The two main pending items are:

1. Merging the MonadLaws and IsDefaultMonad records. I'm happy to do that, but I have not done so yet.
2. The precise definition of def->>->>=. I'm in favor of writing the definition of >> in terms of >>= directly into the type as opposed to relying on a computation. The discussion starts at Reorganize Monad laws, prove Applicative laws #412 (comment) .

[jespercockx]

I don't either change is really essential to merging this PR.

[omelkonian]

@jespercockx If you're fine with Monad-Functor laws being in IsDefaultMonad interface, feel free to merge.

[HeinrichApfelmus]

I will combine MonadLaws and IsDefaultMonad into a single record PreLawfulMonad and then merge later if no one objects.