Dhall-lang: Render Double with given precision

[MICHAELABICK]

Would it possible for there to be a function that renders a Double as Text with a given precision? As an example,

let precision
    : Double → Natural → Text
    = Double/precision

let example0 = assert : precision 3.6 4 ≡ "3.6000"

let example1 = assert : precision -10.506 2 ≡ "-10.51"

in precision

Double/precision was just the first name idea that came to mind -- I am sure someone will have a better idea. Additionally, as shown above, I would prefer to round when reducing precision in my personal use-case, but floor and ceiling are valid alternatives/future work.

[lisael]

What about Double/round, Double/floor and Double/ceil ?

While probably useful, the problem is that it's hard to cover all formatting needs. For example, Double/round 3.14 0 is "3" or "3." ? Double/round 3.14 4 is "3.14" or "3.1400" ?

The next idea is adding a formatting mini language (like python's) for for builtin types, e.g:

{-- here I use python formatting mini-language for the sake of the example --}
let example0 = assert : Double/format ".04" 3.6 ≡ "3.6000"
let example1 = assert : Double/format ".02%" 0.36 ≡ "36.00%"
let example2 = assert : Double/format ".2" -10.506 ≡ "-10.50"
let example3 = assert : Double/format ".2g" -10.506 ≡ "-10.51"

{- other builtin types may expose a builtin format function: -}
let example4 = assert : Bool/format "yes/no" True ≡ "yes"

The big issue of this approach is that the first argument of XXX/format must be a static text that is validated at typecheck. There's no way to do this at the moment. There's also the question: is this too much power ?

[SiriusStarr]

For example, Double/round 3.14 0 is "3" or "3." ? Double/round 3.14 4 is "3.14" or "3.1400" ?

In the former case, "3" presumably is better, since, knowing the behavior, one can always add the period, but since Text currently can't be manipulated, there's no way to get rid of it.

The latter is presumably more open to debate, but my gut would say pad it, i.e. "3.1400", since one is specifying the number of decimal places of precision.

[Gabriel439]

This seems like a safe built-in to add to me in the sense that it converts one opaque type (Double) into another opaque type (Text) and I can see the appeal as we move more templating logic into "pure Dhall" instead of dhall-to-* executables.

@lisael: I probably wouldn't go with a printf-like DSL for formatting for the reason you mentioned: it's a weakly-typed DSL. In particular, the user would not be able to easily infer from the type of such a Double/format primitive whether the format string was well-formed nor would they be able to infer from the type which format options are supported.

@SiriusStarr: Note that Text/replace is close to being standardized in https://github.com/dhall-lang/dhall-lang/pull/1065, so you would be able to fix a trailing . with Text/replace "." "". That said, I agree that it would probably be more aesthetically pleasing for Double/round x 0 to not produce the trailing dot, since it's simpler to add a dot than to use Text/replace to remove the dot. Also, it's more consistent with the language (since Dhall does not permit a trailing . for Double literals).

[Nadrieril]

So far the Foo/show builtins have produced text such that parsing it as a shall expression would give back the original value. For example, Integer/show +3 gives +3 instead of just 3. For consistency I would expect Double/round 3.1 0 to give 3.0 instead of 3 or 3..
I don't know if we want it preserve this kind of behaviour but I thought I'd mention it.

[Gabriel439]

@Nadrieril: I think the main argument for Double/round 3.1 0 not returning 3.0 is that 3.0 is 1 significant digit of precision when the user requested 0 significant digits via the second argument to Double/round. Note that there is not necessarily a contract for Double/round to produce a valid Dhall literal or even a valid Double literal like the Double/show builtin does