module Monoids where

open import Equality

-- Two example monoids

data ℕ : Set where
  zero : ℕ
  succ : ℕ -> ℕ

data ℤ/2 : Set where
  z0 : ℤ/2
  z1 : ℤ/2

-- Addition of natural numbers
addℕ : ℕ -> ℕ -> ℕ
addℕ zero m = m
addℕ (succ n) m = succ (addℕ n m)

assocℕ : ∀ (x y z : ℕ) -> addℕ (addℕ x y) z == addℕ x (addℕ y z)
assocℕ zero y z = refl
assocℕ (succ x) y z = context succ (assocℕ x y z)

-- The left unit law.
left-unit-ℕ : ∀ x -> addℕ zero x == x
left-unit-ℕ x = refl

-- The right unit law.
right-unit-ℕ : ∀ x -> addℕ x zero == x
right-unit-ℕ zero = refl
right-unit-ℕ (succ x) = context succ (right-unit-ℕ x)

-- Addition of Bool ≅ ℤ/(2).
addℤ/2 : ℤ/2 -> ℤ/2 -> ℤ/2
addℤ/2 z0 z0 = z0
addℤ/2 z0 z1 = z1
addℤ/2 z1 z0 = z1
addℤ/2 z1 z1 = z0

-- Associativity
assocℤ/2 : ∀ (x y z : ℤ/2) -> addℤ/2 (addℤ/2 x y) z == addℤ/2 x (addℤ/2 y z)
assocℤ/2 z0 z0 z0 = refl
assocℤ/2 z0 z0 z1 = refl
assocℤ/2 z0 z1 z0 = refl
assocℤ/2 z0 z1 z1 = refl
assocℤ/2 z1 z0 z0 = refl
assocℤ/2 z1 z0 z1 = refl
assocℤ/2 z1 z1 z0 = refl
assocℤ/2 z1 z1 z1 = refl

-- The left unit law.
left-unit-ℤ/2 : ∀ x -> addℤ/2 z0 x == x
left-unit-ℤ/2 z0 = refl
left-unit-ℤ/2 z1 = refl

-- The right unit law.
right-unit-ℤ/2 : ∀ x -> addℤ/2 x z0 == x
right-unit-ℤ/2 z0 = refl
right-unit-ℤ/2 z1 = refl

module Monoid1 where

  -- The following type specifies what it means to be a "monoid
  -- structure" on a set.
  record Monoid (A : Set) : Set where
    field
      plus : A -> A -> A
      unit : A
      associativity-law : ∀ (x y z : A) -> plus (plus x y) z == plus x (plus y z)
      left-unit-law : ∀ (x : A) -> plus unit x == x
      right-unit-law : ∀ (x : A) -> plus x unit == x

  -- Note:
  type-of-plus : {A : Set} → Monoid A → A → A → A
  type-of-plus = Monoid.plus

  module My-Monoids where

    Monoid-ℕ : Monoid ℕ
    Monoid-ℕ = record {
      plus = addℕ;
      unit = zero;
      associativity-law = assocℕ;
      left-unit-law = left-unit-ℕ;
      right-unit-law = right-unit-ℕ
      }

    Monoid-ℤ/2 : Monoid ℤ/2
    Monoid-ℤ/2 = record {
      plus = addℤ/2;
      unit = z0;
      associativity-law = assocℤ/2;
      left-unit-law = left-unit-ℤ/2;
      right-unit-law = right-unit-ℤ/2
      }

  module Monoid-attempt1 where

    open Monoid
    open My-Monoids

    -- Note that the types of plus, unit, etc, take a monoid as an
    -- explicit argument:

    -- plus : {A : Set} → Monoid A → A → A → A
    -- unit : {A : Set} → Monoid A → A

    theorem : ∀ (A : Set) -> (M : Monoid A) -> plus M (unit M) (unit M) == (unit M)
    theorem A M =
      equational plus M (unit M) (unit M)
              by left-unit-law M (unit M)
          equals unit M

    -- Note that at the moment, we can't use infix notation for addition.
    -- Because plus is actually a function of 3 arguments.
    -- plus M x y means "the sum of x and y w.r.t. the monoid structure M"
    -- If we naively defined _+_ = plus, then we'd have to write
    -- "M + x y" because Agda would think that the infix operator
    -- should go between the first two arguments.

  module Monoid-attempt2 where

    -- The notation {{...}} does something magical!
    open Monoid {{...}}

    -- Now check out the type of plus, unit, etc:

    type-of-plus2 : {A : Set} {{ r : Monoid A }} → A → A → A
    type-of-plus2 = plus

    -- What is new is that the monoid structure is a new kind of
    -- implicit argument, called an "instance argument", written with
    -- double curly brackets {{ ... }}.

    -- This kind of argument is called an "instance argument". It is
    -- similar to implicit arguments in that it will be inferred
    -- automatically. It differs in that a different mechanism is used
    -- to do the inference.

    -- We can still write the same theorem as above, specifying M for
    -- each operation:

    theorem1 : ∀ (A : Set) -> {{M : Monoid A}} -> plus {{M}} (unit {{M}}) (unit {{M}}) == (unit {{M}})
    theorem1 A {{M}} =
      equational plus {{M}} (unit {{M}}) (unit {{M}})
              by left-unit-law {{M}} (unit {{M}})
          equals unit {{M}}

    theorem : ∀ (A : Set) -> {{M : Monoid A}} -> plus unit unit == unit
    theorem A =
      equational plus unit unit
              by left-unit-law unit
          equals unit 

    -- Function arguments using {{}} can be omitted. They will be
    -- automatically inferred. This is done by lookup up any monoid
    -- instances that are "known" in the context. Only instances that
    -- are explicitly declared will be found. E.g.: the
    -- {{M : Monoid A}} in the type of "theorem" declares M to be a
    -- monoid instance on the set A. Every time Agda looks for a
    -- monoid structure on A, it will use M. If it looks for a monoid
    -- structure on some other set B, it will not use M.

    proposition : ∀ (A : Set) -> {{M : Monoid A}} -> (x : A) -> plus unit (plus x unit) == x
    proposition A x =
      equational plus unit (plus x unit)
              by left-unit-law (plus x unit)
          equals plus x unit
              by right-unit-law x
          equals x

    module Nat-1 where

      open My-Monoids

      -- How can we use the above proposition, say on the natural
      -- numbers?
      prop-nat : ∀ (n : ℕ) -> plus {{Monoid-ℕ}} (unit {{Monoid-ℕ}}) (plus {{Monoid-ℕ}} n (unit {{Monoid-ℕ}})) == n
      prop-nat n = proposition ℕ {{Monoid-ℕ}} n

      -- The problem here is that when Agda looks for a "canonical"
      -- monoid structure on ℕ, it doesn't find any. Even though
      -- Monoid-ℕ is a monoid structure on ℕ, nothing tells Agda that
      -- it is the one that should be used by default.

    module Nat-2 where

      -- We will declare "canonical" monoid structures on ℕ and ℤ/2 by
      -- using the "instance" keyword.

      instance
        Monoid-ℕ : Monoid ℕ
        Monoid-ℕ = record {
          plus = addℕ;
          unit = zero;
          associativity-law = assocℕ;
          left-unit-law = left-unit-ℕ;
          right-unit-law = right-unit-ℕ
          }

      instance
        Monoid-ℤ/2 : Monoid ℤ/2
        Monoid-ℤ/2 = record {
          plus = addℤ/2;
          unit = z0;
          associativity-law = assocℤ/2;
          left-unit-law = left-unit-ℤ/2;
          right-unit-law = right-unit-ℤ/2
          }
      
      prop-nat : ∀ (n : ℕ) -> plus unit (plus n unit) == n
      prop-nat = proposition ℕ

      prop-ℤ/2 : ∀ (x : ℤ/2) -> plus unit (plus x unit) == x
      prop-ℤ/2 = proposition ℤ/2

      data Color : Set where
        red : Color
        blue : Color
        green : Color

      {- DOES NOT WORK:
      prop-Color : ∀ (c : Color) -> plus unit (plus c unit) == c
      prop-Color = proposition Color
      -} 

module Monoid-with-infix where

  -- The following type specifies what it means to be a "monoid
  -- structure" on a set.
  record Monoid (A : Set) : Set where
    infixl 7 _+_
    field
      _+_ : A -> A -> A
      unit : A
      associativity-law : ∀ {x y z : A} -> (x + y) + z == x + (y + z)
      left-unit-law : ∀ {x : A} -> unit + x == x
      right-unit-law : ∀ {x : A} -> x + unit == x

  open Monoid {{...}}

  proposition : ∀ (A : Set) -> {{M : Monoid A}} -> (x : A) -> unit + (x + unit) == x
  proposition A x =
   equational unit + (x + unit)
           by left-unit-law
       equals x + unit
           by right-unit-law
       equals x

  instance
    Monoid-ℕ : Monoid ℕ
    Monoid-ℕ = record {
      _+_ = addℕ;
      unit = zero;
      associativity-law = λ {x} {y} {z} -> assocℕ x y z;
      left-unit-law = λ {x} -> left-unit-ℕ x;
      right-unit-law = λ {x} -> right-unit-ℕ x
      }

  instance
     Monoid-ℤ/2 : Monoid ℤ/2
     _+_ {{Monoid-ℤ/2}} = addℤ/2
     unit {{Monoid-ℤ/2}} = z0
     associativity-law {{Monoid-ℤ/2}} {x} {y} {z} = assocℤ/2 x y z
     left-unit-law {{Monoid-ℤ/2}} {x} = left-unit-ℤ/2 x
     right-unit-law {{Monoid-ℤ/2}} {x} = right-unit-ℤ/2 x

  open import Logic

  -- Let's define a canonical monoid structure on the cartesian product A × B,
  -- for any sets A, B on which there is already a canonical monoid structure.
  instance
    Monoid-Product : ∀ {A B} -> {{M : Monoid A}} -> {{M' : Monoid B}} -> Monoid (A × B)
    _+_ {{Monoid-Product}} (a1 , b1) (a2 , b2) = ((a1 + a2) , (b1 + b2))
    unit {{Monoid-Product}} = (unit , unit)

    associativity-law ⦃ Monoid-Product ⦄ {(a1 , b1)} {(a2 , b2)} {(a3 , b3)} =
      equational ((a1 + a2) + a3 , (b1 + b2) + b3)
              by cong _,_ associativity-law associativity-law
          equals (a1 + (a2 + a3) , b1 + (b2 + b3))

    left-unit-law {{Monoid-Product}} {(a , b)} =
      equational (unit , unit) + (a , b)
              by cong _,_ left-unit-law left-unit-law
          equals (a , b)

    right-unit-law {{Monoid-Product}} {(a , b)} =
      equational (a , b) + (unit , unit)
              by cong _,_ right-unit-law right-unit-law
          equals (a , b)

  -- Now we have a canonical monoid structure on A × B, whenever
  -- there are canonical monoid structures on A and B.

  myfunc : ℕ × ℕ -> ℕ × ℕ
  myfunc x = x + x

  myfunc2 : ℕ × ℤ/2 -> ℕ × ℤ/2 -> ℕ × ℤ/2
  myfunc2 x y = x + (y + unit) + x

  myfunc3 : ℕ × (ℤ/2 × ℕ) -> ℕ × (ℤ/2 × ℕ)
  myfunc3 x = x + x