# If—

Are losing theirs and blaming it on you,
If you can trust yourself when all men doubt you,
But make allowance for their doubting too.
If you can wait and not be tired by waiting,
Or being lied about, don’t deal in lies,
Or being hated, don’t give way to hating,
And yet don’t look too good, nor talk too wise:

If you can dream—and not make dreams your master;
If you can think—and not make thoughts your aim;
If you can meet with Triumph and Disaster,
And treat those two impostors just the same;
If you can bear to hear the truth you’ve spoken
Twisted by knaves to make a trap for fools,
Or watch the things you gave your life to, broken,
And stoop and build ’em up with worn-out tools:

If you can make a heap of all your winnings
And risk it on one turn of pitch-and-toss,
And lose, and start again at your beginnings
If you can force your heart and nerve and sinew
To serve your turn long after they are gone,
And so hold on when there is nothing in you
Except the Will which says to them: “Hold on!”

If you can talk with crowds and keep your virtue,
Or walk with Kings—nor lose the common touch,
If neither foes nor loving friends can hurt you,
If all men count with you, but none too much;
If you can fill the unforgiving minute
With sixty seconds’ worth of distance run,
Yours is the Earth and everything that’s in it,
And—which is more—you’ll be a Man, my son!

Rudyard Kipling, 1910

# 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.

# Partial orders in Idris

A binary relation $R$ is a partial order if the following properties are satisfied:

1. Reflexivity, i.e. $\forall a, a R a$
2. Transitivity, i.e. $\forall a, b, c, a R b \land b R c \to a R c$
3. Antisymmetry, i.e. $\forall a, b, a R b \land b R a \to a = b$

Let’s abstract this in Idris as an interface:

interface PartialOrder (a : Type) (Order : a -> a -> Type) | Order where
total proofReflexive     : Order n n
total proofTransitive    : Order n m -> Order m p -> Order n p
total proofAntisymmetric : Order n m -> Order m n -> n = m


The interface PartialOrder accepts a Type and a relation Order on it. Since the interface has more than two parameters, we specify that Order is a determining parameter (the parameter used to resolve the instance). Each function definition corresponds to the properties above.

This interface is too abstract as it is, so let’s build a concrete implementation for it:

implementation PartialOrder Nat LTE where
proofReflexive {n = Z}   = LTEZero
proofReflexive {n = S _} = LTESucc proofReflexive

proofTransitive LTEZero           _                 = LTEZero
proofTransitive (LTESucc n_lte_m) (LTESucc m_lte_p) = LTESucc (proofTransitive n_lte_m m_lte_p)

proofAntisymmetric LTEZero           LTEZero           = Refl
proofAntisymmetric (LTESucc n_lte_m) (LTESucc m_lte_n) = let IH = proofAntisymmetric n_lte_m m_lte_n in rewrite IH in Refl


Now you can go and tell your friends that the data type LTE on Nats makes a partial order 🙂