We've tried to force our representations of fractions to have a canonical form, but requiring the inclusion of a proof of that canonical form breaks canonicity.
So we need a different approach.
Data.Rationaldoes it something like this, which I found hard to understand at first. Trying to understand
isCoprimehere was the motivation for this sequence of posts:
record ℚ : Set where field numerator : ℤ denominator-1 : ℕ isCoprime : True (coprime? ( ∣ numerator ∣ ) (suc denominator-1))
isComprimeis different. Rather than directly expressing a proposition (
Coprime numerator (suc denominator-1)) as the type of
isCoprime, we instead use a slightly different proposition (
coprime?) and wrap it in
Decidable Coprime. It is a decidable version of the coprime proposition. A normal proposition type has values that are proofs of that proposition. If I give you a proof, then you know the proposition is true. However, if I don't give you a proof, you don't know that the proposition is false. Perhaps its true but I haven't given you a proof. A decidable proposition type has values that are either proofs that the proposition is true, or proofs that the proposition is false, wrapped in
coprime?is a function that decide whether two numbers are coprime or not, and return a corresponding proof.
Trueis a function that maps a decidable proposition type into another type: either ⊤ (when the proposition is true) or ⊥ (when the proposition is false).
⊤ (top) is the unit type, that has only one member value. ⊥ (bottom) is the empty type with no member values at all.
Both of those seem a bit useless to a traditional programmer: if I have a variable of the unit type ⊤, it can only have one value. So then I'll always know what that value is - its pretty much a constant. So why have a variable? And if I have a variable of the empty type ⊥ then I can't ever invent a value. If that variable is an input parameter, I can never even call my program, because I can't give input parameters. But it turns out this weird behaviour is exactly right for
Say I'm going to construct a half. I'm going to pass
numerator = 1and
denominator = 2. We also need to pass an
To start with, what type of parameter is that?
That depends on the value of numerator and denominator (that's what dependent types are). Once we know the numerator and denominator, we can evaluate the expression
True (coprime? ( ∣ numerator ∣ ) (suc denominator-1))to find out the type of
isCoprime. 1 and 2 are coprime, so
yes _, and so
True (yes _)evaluates to ⊤.
So we need to give a value for coprime that is of type ⊤. ⊤ only has one value, so thats the value that we'll put in
isCoprime. The resulting structure has no proof of coprimality in it. If two fractions have the same numerator and denominator, then they'll always have the same value of isCoprime. So we've got equality of equivalent fractions!
But now what happens if we try to construct a non-canonical fraction, for example 3/6 ?
Once we have specified a numerator of 3 and a denominator of 6, we can figure out the type of
isCoprime. 3 and 6 are not coprime, and
True (no _)will return ⊥.
So we need to provide a value of type ⊥. There are no values in ⊥. So there is no way we can call the constructor in this case, because we can't come up with a value for each parameter.
So now the goal is achieved - a data structure for representing rationals, where equal rationals are definitionally equal.
My goal in picking apart
Data.Rationallike this was two-fold: i) I wanted to use rationals, and wanted to understand what was going on; ii) I want to implement my own canonical forms (for finitely-generated abelian groups) and understanding how its done for rationals seems like a step in the right direction.