Added function to show Rational at a decimal precision

[aortega0703]

#1481 I added functions to show the decimal representation of a Data.Rational (or Data.Rational.Unnormalised) with n decimal digits.

[gallais]

Same comments for the Normalised version too.

[gallais]

We surely want this to return ℤ × Vec ℕ n

[jamesmckinna]

Or even, ℤ × Vec Decimal n, ie. ℤ × Vec (Digit 10) n?

Is it possible (better!?) to re-use any of the functionality in Data.Digit, such as toDigits, rather than computing from scratch? Actually, maybe such an approach would only work for the normalised representation, but I confess I'm no longer clear why unnormalised rationals might need a separate show function, rather than simply 'normalise-then-show'?

[gallais]

We have had bad experiences with Digit being slow hence why I refrained from
suggesting it. Cf. #678

[aortega0703]

I also though about multiplying the fractional part by 10^n, which should give me a ℕ with the first n decimal digits after truncating (and maybe calling toDigits on that?). But the "multiplying by 10^n" part would make the intermediate ℚ have a big numerator so I don't know if that's desirable. Should I do this or use an absolute value and fix the return type?

[jamesmckinna]

Since Vec also supports each of map and concat operations, I'm not sure why you need the extra toList here; moreover, since you already observe that dec here consists of digits (which would appear as one-character Strings), it looks as though there would opportunities to streamline the RHS of this definition? Eg. using Data.String.fromVec?

[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...?

UPDATED: I'm going to lift this out as a separate issue #2946 and not let it get in the way of this PR.

[jamesmckinna]

Thanks very much for this first PR!

Some suggestions and other comments, but I think better to merge sooner rather than later.

[jamesmckinna]

Thanks for doing this.

I realise it violates the 'usual' heuristics of the dependency graph (Data.Rational delegates to/is a normalised wrapper around Data.Rational.Unnormalised), but here I think it does make sense/is the right choice, even if only from a DRY point of view.

[jamesmckinna]

Two things:

• you can streamline the irrefutable pattern match on the with either via let, or perhaps preferable, the new using syntax
• there's an annoying corner case: if dec is [], do you leave the generated string as "" (so, eg "3."), or catch it and render as .0?

For the first:

Suggested change

	showAtPrecision n q with atPrecision n q
	... | (int , dec) = ℤ.show int ++ "." ++ (fromVec (map toDigitChar dec))
	showAtPrecision n q using int , dec ← atPrecision n q
	= ℤ.show int ++ "." ++ (fromVec (map toDigitChar dec))

For the second, I guess I'm not so prescriptive ;-)

[jamesmckinna]

This seems fine on a first pass, ... and premature optimisation is the root of all evil ;-)