fractions and proof-irrelevance II - equality of fractions

This continues from the first in a series of posts reviewing the implementation of Data.Rational in Agda.

We've got a datatype for representing fractions, ensuring that the denominator is strictly positive. So now any element of the mathematical set ℚ can be represented by an element in our datatype ℚ; and vice-versa any element of our datatype ℚ represents an element of the mathematical set ℚ.

Sometimes, we want to be able to compare fractions to see if they are the same or not. It's fairly straightforward to define an equivalence relation between two fractions, using integer multiplication, something like this:

p ≃ q  =  P.numerator ℤ* Q.denominator ≡ Q.numerator ℤ* P.denominator

But sometimes we want to use equivalence where we don't get to specify the equivalence relation. One example of that is type-checking: say we want to use a fraction (for some purpose) as part of a type specification. In that case, we need equivalent fractions to be definitionally equal: they must have been constructed with the same constructor, and the parameters to the constructor must be the same.

The numerator, denominator representation described in the previous post breaks down here: we can represent a half as numerator = 1, denominator = 2; but equally well as numerator = 3, denominator = 6. Yet, 1 ≠ 3 and 2 ≠ 6 so the two representations are not definitionally equal.

One way of solving this is by forcing the representations to be in some canonical form. For fractions, one such form is when the numerator and denominator are co-prime so that there are no shared factors. This way, 1/2 is the canonical representation of a half. 3/6 = (3*1) / (3*2) is not, because 3 is a factor of both the numerator and denominator.

So maybe we could demand that when you call the constructor for a fraction, you have to prove that the numerator and denominator are co-prime, by defining something like this:

record ℚ : Set where
  field
    numerator     : ℤ
    denominator-1 : ℕ
    isCoprime     : Coprime ( | numerator | ) (suc denominator-1)

That way, whenever we construct an element of ℚ, we'll know that the numerator and denominator are co-prime, because we give a proof of the proposition "Coprime numerator denominator" (see that we would add one onto denominator-1 to get the denominator).

Read on for part III...