exports
  Monoid(..)
  empty
  _<>_
  unitMonoid
  additive
  multiplicative
  conjunctive
  disjunctive
  dual
  endo
  reader
  pair

import Num

-- The Monoid type

record Monoid m
  .empty  m
  .append (m -> m -> m)

-- implicit sugars for the Monoid operations

empty : implicit (Monoid m) -> m
  m = m.empty

_<>_ : m -> m -> implicit (Monoid m) -> m
  x y m = m.append x y

-- some Monoid values

implicit unitMonoid : Monoid () = rec
  .empty      = ()
  .append _ _ = ()

additive : implicit (Add m) -> Monoid m
  add = rec .empty  = add.zero
            .append = add.plus

multiplicative : implicit (Mul m) -> Monoid m
  mul = rec .empty  = mul.one
            .append = mul.times

implicit conjunctive : Monoid Bool = rec
  .empty  = False
  .append = _&&_

disjunctive : Monoid Bool = rec
  .empty  = True
  .append = _||_

dual : Monoid m -> Monoid m
  m = rec .empty      = m.empty
          .append x y = m.append y x

endo : Monoid (a -> a) = rec
  .empty      = id
  .append x y = compose x y

reader : implicit (Monoid b) -> Monoid (a -> b)
  m = rec .empty _ = m.empty
          .append x f g = m.append (f x) (g x)

pair : implicit (Monoid l) -> implicit (Monoid r) -> Monoid (l * r)
  l r = rec .empty = (l.empty, r.empty)
            .append (x1, y1) (x2, y2) = (l.append x1 x2, r.append y1 y2)