# Binary Relations in Idris

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.