Partial orders in Idris

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

1. Reflexivity, i.e.
2. Transitivity, i.e.
3. Antisymmetry, i.e.

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 🙂