Floats vs JsonNumber

Stream: lean4

[Adam Topaz]

I'm planning on doing some (very mild) computations with some floats that will be fetched from some external API.
These numbers are parsed as JsonNumbers but it seems that this type doesn't support any arithmetic operations.
If I convert this JsonNumber to a float and back, it seems to lose some information. E.g.:

def bar : JsonNumber := 0.12398711
#eval bar
-- ⟨12398711,8⟩
#eval JsonNumber.fromFloat? <$> ((fromJson? <| .num bar) : Except String Float)
-- Except.ok (Sum.inr ⟨123987,6⟩)

Is there some way to make this operation lossless?

[Adam Topaz]

Or a more general question: What's the preferred way to calculate with numbers from a Json object?

[Adam Topaz]

Adam Topaz said:

Is there some way to make this operation lossless?

Of course the answer is no, based on how JsonNumber is defined.

[Adam Topaz]

Perhaps more to the point: has someone implemented double precision floats somewhere?

[Mac Malone]

Adam Topaz said:

Perhaps more to the point: has someone implemented double precision floats somewhere?

Float is double

[Adam Topaz]

Ok now I'm confused.

[Adam Topaz]

Why then is my number in the above example truncated to 6 decimal places?

[Gabriel Ebner]

Obviously because toString truncates to 6 decimal places:

/-- Creates a json number from a positive float, panicking if it isn't.
[todo]EdAyers: Currently goes via a string representation, when more float primitives are available
should switch to using those. -/
private def fromPositiveFloat! (x : Float) : JsonNumber :=
  match Lean.Syntax.decodeScientificLitVal? (toString x) with
  | none => panic! s!"Failed to parse {toString x}"
  | some (m, sign, e) => OfScientific.ofScientific m sign e

[Mac Malone]

Also note that this can be observed from just the following:

#eval bar.toFloat
-- 0.123987

[Mac Malone]

To see that toString rounds to 6 decimal places, observe:

#eval bar.toFloat * 100
-- 12.398711

[Adam Topaz]

Ah ok I see

[Adam Topaz]

I missed that comment :)

[Adam Topaz]

But this is a problem isn’t it? Any time we make a JSON from something with floats the numbers will get truncated.

[Adam Topaz]

Or is there some separate ToJson instance for floats?

[Jason Rute]

I guess the question is if “when more float primatives are available”, is now or the future?

[Gabriel Ebner]

No the ToJson Float instance unfortunately uses fromFloat?.

[Gabriel Ebner]

I think this counts as a bug. It's not just number of digits either. Numbers like 1e-15 are truncated as well.

[Gabriel Ebner]

If I wanted to add a proper ToJson instance for float using the current API, I'd extract the exponent using (f.abs.log2 + 2048).toUInt32 - 2048, then get the mantissa using f.scaleB (60 - e) |>.toUInt64 and then piece that together as a JsonNumber.

[Mario Carneiro]

I could have sworn I added a primitive for extracting parts of a float

[Mario Carneiro]

docs4#Float.frExp

[Gabriel Ebner]

I briefly looked at frExp, but you still need to extract the mantissa manually (and fiddle with the signs because we don't have Float.toInt64) so it doesn't help much.