currently numbers default to 32 bit floats, but this can lead to loss of information as JSON numbers are 64 bit float

there is an existing solution (add format: double everywhere), but this (at least for our current use case) will be very cumbersome

note: added optional default value in #1913