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.Rational`

does it something like this, which I found hard to understand at first. Trying to understand `isCoprime`

here was the motivation for this sequence of posts:record ℚ : Set where field numerator : ℤ denominator-1 : ℕ isCoprime : True (coprime? ( ∣ numerator ∣ ) (suc denominator-1))

`isComprime`

is 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 `True`

.`coprime?`

has type `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

`yes`

or `no`

respectively. `coprime?`

is a function that *decide*whether two numbers are coprime or not, and return a corresponding proof.

`True`

is 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

`Data.Rational`

.Say I'm going to construct a half. I'm going to pass

`numerator = 1`

and `denominator = 2`

. We also need to pass an `isCoprime`

parameter.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 `coprime?`

evaluates to `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.Rational`

like 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.
## No comments:

## Post a Comment