[ refactor / design ] primitive operations on `Data.Rational` which get used in anger as computations

[jamesmckinna]

I'm definitely perturbed by

• p ≤ᵇ 0ℚ in the definition of truncate, when strictly-less-than would make more sense (because/and avoid needless fumbling at 0ℚ...)
• the lack of sharing between truncate and fracPart in definitions where both operations are deployed, as here

Such concerns are, strictly speaking, out of scope for this PR, but I think we should bear them in mind when implementing (internal) computations intended to be used 'in anger', such as show functions...?

Originally posted by @jamesmckinna in #2945 (comment)

I reasoned as follows:

• working constructively, it has never made sense to me to work with weaker observations, when stronger/more positive would be 'better': but here, we don't have (the obviously analogous) definition of p <ᵇ 0ℚ... so perhaps we should!?
• fracPart uses truncate, so as with analogous operations such as division-with-remainder [ add ] a 'better' division with remainder for Data.Integer.Base #2878 , it might make sense to bundle them as a pair, and then project?

[jamesmckinna]

First thoughts (though it seems as they have been thought before): using Data.Refinement, introduce

• ℚ⁺ = [ p ∈ ℚ | Positive p ] (or some variation thereof)
• [0,1) = [ p ∈ ℚ | NonNegative p ∧ p < 1ℚ ] ...

and then

• fracPart : ℚ → [0,1)
• implement truncate : ℚ → ℤ as now (and profit from the fraction being in lowest terms)
• avoid implementing ℚᵘ.truncate and ℚᵘ.fracPart altogether? (we prove no properties of these functions, whether normalised or not)

or even

• (0,1) = [ p ∈ ℚ⁺ | p < 1ℚ ] (plus some plumbing for iterated Refinements)
• [truncate,fracPart] as a view of ℚ as ℤ × Maybe (0,1)... or something?

[aortega0703]

Today I was proving some properties of the rounding functions and when trying to prove truncate q + fracPart q = q I realized that this doesn't hold for the current definition

• fracPart q = | q - truncate q |

In Wolfram they seem to rather use

• fracPart q = q - truncate q (without the abs)

to preserve this property (pretty much by definition). This would change the range from [0, 1) to (-1, 1), but maybe then it would make even more sense to pack those functions together?

[jamesmckinna]

Good spot!

I've never really done much with stdlib rationals (besides bureaucratic refactoring and some 'logical'/order-theoretic stuff), so this issue was really a placeholder to query some of the current implementation ideas wrt "what spec do we expect these things to confirm to, anyway!?"

So definitely I think this is worth a bit more investigation... but downstream of your current PR!!!

[jamesmckinna]

Eg: for normalised rationals, I guess Wolfram-style truncate/fracPart can be computed entirely in terms of Integer divMod, and looking at optimising that cf. #2878 but the devil is in the details!?

[jamesmckinna]

See also #2945 (review)