monoid.ml

open StdLabels

let id x = x
let (>>) f g a = g (f a)

let for_all ~set f = 
  List.iter ~f:(fun x -> assert (f x)) set

let for_all2 ~set f = 
  for_all ~set (fun a -> 
    for_all ~set (f a))

let for_all3 ~set f = 
  for_all ~set (fun a -> 
    for_all ~set (fun b -> 
      for_all ~set (f a b)))

module type MONOID = sig
  type t

  val empty: t
  val append: t -> t -> t
end 

module False_monoid: MONOID = struct
  type t = bool
  let set = [true; false]

  let empty = false

  let append left right = (* && *)
    if left then right = true else false
  
  let (^) = append

  let () = for_all ~set @@ fun a -> 
    empty ^ a = a ^ empty;
(*
  Proof:
    empty ^ a === a ^ empty
    if false then a = true else false === if a then empty = true else false
    false === if a then false = true else false
    false === if a then false else false
    false === false
*)

  let () = for_all3 ~set @@ fun a b c -> 
    (a ^ b) ^ c = a ^ (b ^ c);
(*
  Proof:
    (a ^ b) ^ c === a ^ (b ^ c)
    if (if a then b = true else false) then c = true else false
      === if a then (if b then c = true else false) = true else false
    if a 
      then (if (if a then b = true else false) then c = true else false)
      else (if (if a then b = true else false) then c = true else false)
      === if a then (if b then c = true else false) = true else false
    if a 
      then (if b = true then c = true else false)
      else (if false then c = true else false)
      === if a then (if b then c = true else false) = true else false
    if a 
      then (if b = true then c = true else false)
      else false
      === if a then (if b then c = true else false) = true else false
    if a 
      then (if b = true then c = true else false)
      else false
      === if a 
            then (if b then c = true else false) = true 
            else false
    if b = true then c = true else false
      === (if b then c = true else false) = true 
    if b = true then c = true else false
      === if b then (c = true) = true else (false = true)
    if b = true then c = true else false
      === if b then c = true else false
    if b then c = true else false
      === if b then c = true else false
 *)
end

module Modulo_3_arithmetic: MONOID = struct
  type t = Zero | One | Two
  let set = [Zero; One; Two]

  let empty = Zero

  let increment = function
    | Zero -> One
    | One -> Two
    | Two -> Zero

  let append = function
    | Zero -> id
    | One -> increment
    | Two -> increment >> increment

  let (^) = append

  let () = for_all ~set @@ fun a -> 
    (empty ^ a) = (a ^ empty);
(*  
  Proof:
    empty ^ a === a ^ empty
    Zero ^ a === a ^ Zero
    id a === a ^ Zero
    a === (function 
      | Zero -> id Zero
      | One -> increment Zero
      | Two -> increment (increment Zero)
    ) a
    a === (function 
      | Zero -> Zero
      | One -> One
      | Two -> increment One
    ) a
    a === (function
      | Zero -> Zero
      | One -> One
      | Two -> Two
    ) a
    a === id a
    a === a
*)
  let () = for_all3 ~set @@ fun a b c -> 
    (a ^ b) ^ c = a ^ (b ^ c);
end