A comparison of implementing a Monoid type using 1) Idris Sigma types, 2) an Idris dependent record, 3) an Agda dependent record

1-monoid-sigma.idr

BinOp : (A : Type) -> Type
BinOp A = A -> A -> A

parameters ((*) : BinOp a)
  IsAssociative : Type
  IsAssociative = (x, y, z : _) -> x * (y * z) = (x * y) * z

  IsLeftIdentity : a -> Type
  IsLeftIdentity e = (x : _) -> e * x = x

  IsRightIdentity : a -> Type
  IsRightIdentity e = (x : _) -> x * e = x

  IsIdentity : a -> Type
  IsIdentity e = (IsLeftIdentity e, IsRightIdentity e)

Monoid : Type
Monoid =
  Sigma Type      $ \M  =>
  Sigma (BinOp M) $ \op =>
  Sigma M         $ \e  =>
  (IsAssociative op, IsIdentity op e)

parameters (m : Monoid)
  
  -- Accessors

  monSet : Type
  monSet = case m of (M ** _) => M

  monOp : monSet -> monSet -> monSet
  monOp = case m of (_ ** (op ** _)) => op

  monUnit : monSet
  monUnit = case m of (_ ** (_ ** (e ** _))) => e

  monOpIsAssociative    : IsAssociative monOp
  monOpIsAssociative    = case m of (_ ** (_ ** (_ ** (p, _, _)))) => p

  monUnitIsLeftIdentity   : IsLeftIdentity monOp monUnit
  monUnitIsLeftIdentity   = case m of (_ ** (_ ** (_ ** (_, p, _)))) => p

  monUnitIsRightIdentity  : IsRightIdentity monOp monUnit
  monUnitIsRightIdentity  = case m of (_ ** (_ ** (_ ** (_, _, p)))) => p

  -- Theorems

  monUnitIsUniqueLeftIdentity : (e2 : monSet) -> IsLeftIdentity monOp e2 -> e2 = monUnit
  monUnitIsUniqueLeftIdentity e2 e2Left = trans lemma1 lemma2
    where
      lemma1 : e2 = e2 `monOp` monUnit
      lemma1 = sym (monUnitIsRightIdentity e2)

      lemma2 : e2 `monOp` monUnit = monUnit
      lemma2 = e2Left monUnit

  monUnitIsUniqueRightIdentity : (e2 : monSet) -> IsRightIdentity monOp e2 -> e2 = monUnit
  monUnitIsUniqueRightIdentity e2 e2Left = trans lemma1 lemma2
    where
      lemma1 : e2 = monUnit `monOp` e2
      lemma1 = sym (monUnitIsLeftIdentity e2)

      lemma2 : monUnit `monOp` e2 = monUnit
      lemma2 = e2Left monUnit

-- Instances

NatAddMonoid : Monoid
NatAddMonoid = (Nat ** ((+) ** (Z ** (plusAssociative, plusZeroLeftNeutral, plusZeroRightNeutral))))

NatMultMonoid : Monoid
NatMultMonoid = (Nat ** ((*) ** (S Z ** (multAssociative, multOneLeftNeutral, multOneRightNeutral))))

ListMonoid : Type -> Monoid
ListMonoid A = (List A ** ((++) ** ([] ** (appendAssociative, \xs => refl, appendNilRightNeutral))))

2-monoid-record.idr

-- This one looks cleaner than the Sigma version, but has the disadvantage
-- that Idris emits warnings for the fact that it can't generate the dependent
-- record accessors.

BinOp : (A : Type) -> Type
BinOp A = A -> A -> A

parameters ((*) : BinOp a)
  IsAssociative : Type
  IsAssociative = (x, y, z : _) -> x * (y * z) = (x * y) * z

  IsLeftIdentity : a -> Type
  IsLeftIdentity e = (x : _) -> e * x = x

  IsRightIdentity : a -> Type
  IsRightIdentity e = (x : _) -> x * e = x

  IsIdentity : a -> Type
  IsIdentity e = (IsLeftIdentity e, IsRightIdentity e)

record Monoid : Type where
  MkMonoid : (M  : Type) ->
             (op : BinOp M) ->
             (e  : M) ->
             IsAssociative   op ->
             IsLeftIdentity  op e ->
             IsRightIdentity op e ->
             Monoid

parameters (m : Monoid)
  
  -- Accessors (should ideally be autogenerated by the record declaration!)

  monSet : Type
  monSet = case m of MkMonoid M _ _ _ _ _ => M

  monOp : monSet -> monSet -> monSet
  monOp = case m of MkMonoid _ op _ _ _ _ => op

  monUnit : monSet
  monUnit = case m of MkMonoid _ _ e _ _ _ => e

  monOpIsAssociative     : IsAssociative monOp
  monOpIsAssociative     = case m of MkMonoid _ _ _ p _ _ => p

  monUnitIsLeftIdentity  : IsLeftIdentity monOp monUnit
  monUnitIsLeftIdentity  = case m of MkMonoid _ _ _ _ p _ => p

  monUnitIsRightIdentity : IsRightIdentity monOp monUnit
  monUnitIsRightIdentity = case m of MkMonoid _ _ _ _ _ p => p

  -- Theorems

  monUnitIsUniqueLeftIdentity : (e2 : monSet) -> IsLeftIdentity monOp e2 -> e2 = monUnit
  monUnitIsUniqueLeftIdentity e2 e2Left = trans lemma1 lemma2
    where
      lemma1 : e2 = e2 `monOp` monUnit
      lemma1 = sym (monUnitIsRightIdentity e2)

      lemma2 : e2 `monOp` monUnit = monUnit
      lemma2 = e2Left monUnit

  monUnitIsUniqueRightIdentity : (e2 : monSet) -> IsRightIdentity monOp e2 -> e2 = monUnit
  monUnitIsUniqueRightIdentity e2 e2Left = trans lemma1 lemma2
    where
      lemma1 : e2 = monUnit `monOp` e2
      lemma1 = sym (monUnitIsLeftIdentity e2)

      lemma2 : monUnit `monOp` e2 = monUnit
      lemma2 = e2Left monUnit

-- Instances

NatAddMonoid : Monoid
NatAddMonoid = MkMonoid Nat (+) Z plusAssociative plusZeroLeftNeutral plusZeroRightNeutral

NatMultMonoid : Monoid
NatMultMonoid = MkMonoid Nat (*) (S Z) multAssociative multOneLeftNeutral multOneRightNeutral

ListMonoid : Type -> Monoid
ListMonoid A = MkMonoid (List A) (++) [] appendAssociative (\xs => refl) appendNilRightNeutral

3-monoid-record.agda

-- Agda records are awesome, and the unicode support is nice too

infixl 3 _==_
data _==_ {A : Set} (x : A) : A -> Set where
  refl : x == x

_<trans>_ : {A : Set} {x y z : A} -> x == y -> y == z -> x == z
refl <trans> refl = refl

sym : {A : Set} {x y : A} -> x == y -> y == x
sym refl = refl

cong : {a b : Set} {x y : a} {f : a -> b} -> (x == y) -> (f x == f y)
cong refl = refl

record Monoid : Set1 where
  field
    M   : Set
    _•_ : M -> M -> M
    ε   : M
    x•[y•z]=[x•y]•z : forall x y z -> x • (y • z) == (x • y) • z
    ε•x=x           : forall x -> ε • x == x
    x•ε=x           : forall x -> x • ε == x

  ε-is-unique-left-id : (ε₂ : M) -> (forall x -> ε₂ • x == x) -> ε₂ == ε
  ε-is-unique-left-id ε₂ ε₂•x=x = sym (x•ε=x ε₂) <trans> ε₂•x=x ε

  ε-is-unique-right-id : (ε₂ : M) -> (forall x -> x • ε₂ == x) -> ε₂ == ε
  ε-is-unique-right-id ε₂ x•ε₂=x = sym (ε•x=x ε₂) <trans> x•ε₂=x ε

data Nat : Set where
  Z : Nat
  S : Nat -> Nat

infixl 6 _+_
_+_ : Nat -> Nat -> Nat
Z + n = n
S n + m = S (n + m)

n+[m+k]=[n+m]+k : forall n m k -> n + (m + k) == (n + m) + k
n+[m+k]=[n+m]+k Z _ _ = refl
n+[m+k]=[n+m]+k (S n) m k = cong {f = S} (n+[m+k]=[n+m]+k n m k)

Z+n=n : forall n -> Z + n == n
Z+n=n _ = refl

n+Z=Z : forall n -> n + Z == n
n+Z=Z Z = refl
n+Z=Z (S n) with n + Z | n+Z=Z n
... | .n | refl = refl

[Nat,+,Z] : Monoid
[Nat,+,Z] = record 
  { M   = Nat
  ; _•_ = _+_
  ; ε   = Z
  ; x•[y•z]=[x•y]•z = n+[m+k]=[n+m]+k
  ; ε•x=x           = Z+n=n
  ; x•ε=x           = n+Z=Z
  }