Every natural number is either zero or the successor of some number. In Idris this is expressed as a type:

Given two numbers m and n, m ≤ n (that is, m is less than or equal to n) either when m is zero or when m is the successor of j and n is the successor of k and j ≤ k. This is again expressed in Idris as a type:

≤ is the classic example of a binary relation. In type theory a binary relation is a function of type `ty -> ty -> Type`. This is not to be confused with binary operation, which is a function of type `ty -> ty -> ty`. Binary operations produce instances of some type, but binary relations produce things that are themselves types. In spirit a binary relation is similar to a function of type `ty -> ty -> Bool`; it is a proposition that “says” something that may or may not be true.

Certain common properties are used to classify binary relations and describe their behavior. For example, ≤ is reflexive: x ≤ x for all x. It is also transitive and antisymmetric: if x ≤ y and y ≤ z then x ≤ z; and x ≤ y and y ≤ x only when x = y.

In idris these properties are expressed with interfaces:

Implementing these interfaces for a relation over some type verifies that the relation bears those properties. Sometimes this is difficult, and sometimes it’s easy:

A preorder is a relation that is both reflexive and transitive, and a partial order is a preorder that is antisymmetric:

These order properties are empty – just definitions that bundle together other properties. Consequently they are easy to implement:

A slightly more complicated property is connexity. A relation is connex over a type if any two distinct instances of the type are related one way or another, and a linear order is a connex partial order:

≤ is connex over the naturals, but this is trickier to prove than the other properties:

≤ is antisymmetric: x ≤ y implies y ≤ x only when y = x. A relation is symmetric when it goes both ways unconditionally:

A simple example of a symmetric relation is the relation of being-within-one-of:

If x is within one of y, then y is within one of x. Further, x is within one of x for all x:

A relation that is both reflexive and symmetric is a tolerance relation:

The within-one-of relation is not transitive. 2 is within one of 3 and 4 is within one of 3, but 2 is not within one of 4. A tolerance relation that is transitive is an equivalence relation. This could also be defined as a symmetric preorder. Or even better, forget about the hierarchy altogether and define an equivalence relation directly as a bundle of reflexive, transitive, and symmetric:

Let p be a factor of q and let q be factor of r. Is p a factor of r? Yes, and therefore the is-a-factor-of relation is transitive. It’s also reflexive and antisymmetric, and so the relation is another example of a partial order. All of these claims can be proved in Idris, although it takes some work:

Reflexivity, transitivity, and symmetry are the most prominent properties of binary relations. A lesser-known property is density: a relation is dense if between any two related elements there is a third related element:

Every reflexive relation is dense: if x is related to y, then by reflexivity x is related to x, and so x itself serves as the intercalated element:

So ≤ is technically dense, but that doesn’t mean much. The strictly-less-than relation < is not dense over the natural numbers: 3 < 4, but there is no x such that 3 < x and x < 4. But it is dense over the rational numbers: if a/b < c/d, then a+c/b+d comes between them.

A relation such that x being related to y and also to z implies that y is related to z is called Euclidean:

Euclideanness is commonly listed as a property of relations, but examples are hard to come by. The Wikipedia page for Euclidean relations doesn’t list any! Still, a few general properties can be proved. If a Euclidean relation is reflexive, it is also symmetric; and if it is reflexive, it is also transitive. Finally, a relation that is both transitive and symmetric is Euclidean:

As of v0.5, all of these relations and more are included in the Idris 2 standard library. I authored the current design. Earlier version of Idris used a different relation module with fewer relations and an inflexible hierarchy of order relations.