Generating a random float number?

Stream: new members

[Youngju Song]

Is there a way to generate a random float number, like Python's random()? (using uniform distribution)

[Kevin Buzzard]

You mean "there are only finitely many floats so pick one at random with every one having equal probability"? Is that what "uniform" means in this context?

[Kyle Miller]

@Kevin Buzzard Generally these random float functions generate a random number in [0.0,1.0) uniformly at random. That's what Python's random() does at least.

[Kevin Buzzard]

Oh I was about to come up with something using docs#Float.ofScientific and docs#randNat ;-)

[Youngju Song]

@Kevin Buzzard I guess no, I want something that usual libraries in programming languages would do. In my understanding, Python's random() behaves like: sampling an element over the uniform distribution in Real numbers (in interval [0,1)) and getting the closest Float representation for that.

[Kevin Buzzard]

Yes that would be a lot more sensible!

[Youngju Song]

At the moment I am doing:

do
  let x ← IO.rand 0 (2^64-1)
  return (x.toFloat / (2^64-1))

but I guess there is a better way than this.

[Eric Wieser]

What meaning of "better" are you after?

[Henrik Böving]

If you want to implement exactly what python's random does (which is btw. of course not related at all to real numbers):

BPF = 53        # Number of bits in a float
RECIP_BPF = 2 ** -BPF

    def random(self):
        """Get the next random number in the range 0.0 <= X < 1.0."""
        return (int.from_bytes(_urandom(7)) >> 3) * RECIP_BPF

you can use

def bpf : Nat := 53
def recip_bfp : Float := 2 ^ (-Float.ofNat bpf)


def random : IO Float := do
  let base := ByteArray.mk #[0]
  let int := base ++ (← IO.getRandomBytes 7) |>.toUInt64BE!

  return (int >>> 3).toNat.toFloat * recip_bfp


#eval random

Note that this not exactly as good as python because their implementation uses urandom whereas getRandomBytes is not guaranteed to be cryptographically secure but it should be acceptable for statistical experimentation.

[Eric Wieser]

"Number of bits in a float" seems like a strange comment

[Eric Wieser]

Youngju Song said:

sampling an element over the uniform distribution in Real numbers (in interval [0,1)) and getting the closest Float representation for that.

This is not what your code or python does; neither will ever sample 2^-1074

[Henrik Böving]

Eric Wieser said:

"Number of bits in a float" seems like a strange comment

I'm just copying python source code here :P besides, the mantissa is of that length so that's likely what they are after here.

[Youngju Song]

Thank you for the comments!

What meaning of "better" are you after?

I was expecting the random libraries e.g., in Python to implement some serious complicated black-box algorithm to sample as faithfully as possible to Real numbers, but as @Henrik Böving brought up here, the implementation in Python is (to my surprise) rather straightforward! I am happy with whatever implementation that is as good as Python's. Thank you very much for your code @Henrik Böving !

[Youngju Song]

@Henrik Böving Maybe it is worth putting your implementation to the Lean's standard library?

[Henrik Böving]

It could be in principle but I don't think this does justice to what we'd want in Std. Ideally there would be some random monad that can be fed with IO.getRandomBytes among other things and then we can build generically on top of that so I don't think I'll put this code into Std as is.

[Dominic Steinitz]

You could usefully take a look at the Haskell random number library and its monadic counterpart. We spent a lot of time on its design as an interface allowing users (should they so wish) to use their own source of randomness: https://hackage.haskell.org/package/random-1.3.0/docs/System-Random-Stateful.html#g:21 and https://hackage.haskell.org/package/random-1.3.0/docs/System-Random.html#g:16. See especially the caveats on floating point.

Of course, it all depends on what you want random numbers for. The default implementation passes most of the standard (pseudo) random number generator tests: https://github.com/tweag/random-quality (I recommend using these to check the quality of your implementation). Good enough for pricing financial derivatives but not maybe for cryptographic applications.

This is an area that sounds straightforward but will take you on a long journey.

[Dominic Steinitz]

Youngju Song said:

Kevin Buzzard I guess no, I want something that usual libraries in programming languages would do. In my understanding, Python's random() behaves like: sampling an element over the uniform distribution in Real numbers (in interval [0,1)) and getting the closest Float representation for that.

And Floating Point is its own rabbit hole. You should think about a mantissa with 3 bits and exponent of 2 bits for example to get a feel for how they are distributed. And as everyone knows they don't even obey the usual arithmetical laws.

[Philippe Duchon]

Henrik Böving said:

If you want to implement exactly what python's random does (which is btw. of course not related at all to real numbers):

Also, this is not guaranteed to output the closest floating point number to a "random real in the range $[0,1)$". If the result is close to 0 where the floats are closer together, using a fixed number of random bits will result in truncation in the mantissa. If I read correctly your example code it uses 56 random bits, and this is only 3 more than the mantissa length in a float, so a small but not negligible of random floats obtained this way will have fixed 0 bits at the end of their mantissa.

(I don't think there are many standard libraries that try to deal with this issue, as using a non-fixed number of random bits would likely increase run times; I don't know if the need for cryptographic-level random floats is that high either)

[Eric Wieser]

Philippe Duchon said:

If I read correctly your example code it uses 56 random bits, and this is only 3 more than the mantissa length in a float, so a small but not negligible of random floats obtained this way will have fixed 0 bits at the end of their mantissa.

It generates exactly 53 random bits (it immediately discards 3 of the 56), so I think "small" here is 50% of random floats having at least one fixed zero bit in the mantissa