Proving Monoids with Idris

I was watching an interesting video, Opening Keynote by Edward Kmett at Lambda World 2018. Note in the beginning of that video how in Haskell you’d put code comments in place of proofs.

Enter Idris.

As a short example, we can abstract a proven Monoid as an interface:

interface ProvenMonoid m where
	mappend : m -> m -> m
	mempty  : m
	assocProof : (a, b, c : m) -> mappend a (mappend b c) = mappend (mappend a b) c
	idProofL   : (a : m) -> mappend mempty a = a
	idProofR   : (a : m) -> mappend a mempty = a

Do Nats make a Monoid? Sure they do, and here’s the proof for that:

implementation ProvenMonoid Nat where
	mappend x y = x + y
	mempty      = 0

	-- Proofs that this monoid is really a monoid.
	assocProof  = plusAssociative
	idProofL    = plusZeroLeftNeutral
	idProofR    = plusZeroRightNeutral

Note that plusAssociative, plusZeroLeftNeutral, and plusZeroRightNeutral are already part of Idris’ prelude. In the next example we’ll do an actual proof ourselves instead of re-using existing proofs.

What about List of Nats? Yep.

implementation ProvenMonoid (List Nat) where
	mappend x y = x ++ y
	mempty      = []

	-- Proofs that this monoid is really a monoid.
	assocProof [] b c      = Refl
	assocProof (a::as) b c = rewrite assocProof as b c in Refl
	idProofL a             = Refl
	idProofR []            = Refl
	idProofR (x::xs)       = rewrite idProofR xs in Refl

Some valid questions are:

• Why should I care about monoids?
  • Edward covers this in the video at around 3:00.
• Why should I care about proving monoids?
  • Let’s assume that there’s an algorithm running in production that relies on Monoids. What we don’t want to happen is associativity to break, because if it does then the “combine” function applied on all of the produced results will likely be wrong.

🙂

EDIT: Updated first example per u/gallais’s comment.