Here are some type-level definitions of parity functions written in Idris:

Given some natural number `n`, `Even n` says that there exists a number `half` such that `n` is equal to `half` times two, while `Odd n` says that there exists a number `haf` such that `n` one more than `haf` times two. (These definitions, along with the “haf” terminology, come from The Little Typer.)

`Even n` doesn’t prove that `n` is even, it just makes the claim that it is. A proof of this claim (or equivelently, an instance of the type) takes the form of a dependent pair, a witness together with a proof that the witness satisfies the stated condition. A witness is required because dependently-typed languages like Idris use constructive logic.

It can be proved without too much trouble that the sum of two even numbers is also even:

The type signature there says: given a proof that `j` is even and a proof that `k` is even, produce a proof that `j + k` is even. So we’re given numbers `half_j` and `half_k`, plus proofs that `j = half_j * 2` and `k = half_k * 2`, and the goal is to produce a witness such that `j + k` is equal to the witness times two. The first line in the implementation shows that the witness is the sum of the two halves.

The rest of the implementation is the proof, the details of which can be illustrated with a simple example: `6 + 8 = (3 * 2) + (4 * 2) = (3 + 4) * 2`. The last line in the proof, an instance of `multDistributesOverPlusLeft`, is what moves from `(3 * 2) + (4 * 2)` to `(3 + 4) * 2`. It’s not an interesting part of the proof, but it’s needed to appease the type checker.

It can also be proved without too much trouble that the sum of an odd number and an even number is odd:

This proof looks almost exactly like that of `evenPlusEven`, except for an extra line. That line handles the odd one. Another example might make it clear, and again the arithmetic looks almost the same as before: `7 + 8 = 1 + 6 + 8 = 1 + (3 * 2) + (4 * 2) = 1 + (3 * 2) + (4 * 2) = 1 + ((3 + 4) * 2)`.

This is repetitive code, and repetitive code is bad. In particular, the repeated invocation of the low-level number-shuffler `multDistributesOverPlusLeft` grates. That work was done before, so why do it again?

There is a better way. First, observe that any odd number is the successor of an even number:

Then, instead of proving `oddPlusEven` from scratch, extract an even number from the odd and then add it to the other even number using the already-proved `evenPlusEven`:

To my taste, this is a nicer proof. The initial proof arguments are passed intact into other functions rather than being destructured, a sign that computation is taking place elsewhere. Everything is at the appropriate level of abstraction, and there is no annoying algebra to deal with.

Maybe it’s an obvious point, but I haven’t seen it discussed anywhere, so I’ll make it plain: dependently-typed proofs are code, and repetitive code is bad, so repetitive dependently-typed proofs are bad.