Add lawful subclasses of existing type classes

It would be good to have standard definitions of the type class laws for the classes in the Prelude, and prove them for the instances we provide. Here is an example of how this would look:

open import Haskell.Prelude

record LawfulMonad (m : Set → Set) {{iMonad : Monad m}} : Set₁ where
  field
    left-id  : ∀ {a b} (x : a) (f : a → m b)
             → (return x >>= f) ≡ f x
    right-id : ∀ {a} (k : m a)
             → (k >>= return) ≡ k
    assoc    : ∀ {a b c} (k : m a) (f : a → m b) (g : b → m c)
             → ((k >>= f) >>= g) ≡ (k >>= (λ x → f x >>= g))
open LawfulMonad

instance
  _ : LawfulMonad Maybe
  _ = λ where
    .left-id → λ x f → refl
    .right-id Nothing → refl
    .right-id (Just x) → refl
    .assoc Nothing f g → refl
    .assoc (Just x) f g → refl

Classes for which we should define laws:

[x] Eq and Ord
[x] Num
[ ] BoundedBelow, BoundedAbove, and Bounded
[ ] Enum
[x] Semigroup and Monoid
[x] Functor, Applicative, and Monad
[ ] Foldable and Traversable

agda / agda2hs

Add lawful subclasses of existing type classes #108