inhabited instance for StdGen isn't very random

Stream: new members

[Michael MacLeod]

I am very confused by the fact that stdNext seems to return its input unchanged when its input is (default : StdGen). Is this really the intended behavior?

I ran into this problem when I was having trouble producing different random numbers using randNat.

Lean 4 Web example

#eval do
  let gen : StdGen := default
  let (a, gen) := randNat gen 0 10000
  let (b, gen) := randNat gen 0 10000
  let (c, gen) := randNat gen 0 10000
  let (d, gen) := randNat gen 0 10000
  let (e, gen) := randNat gen 0 10000
  let (f,   _) := randNat gen 0 10000
  IO.println s!"{a}" -- 8835
  IO.println s!"{b}" -- 8835
  IO.println s!"{c}" -- 8835
  IO.println s!"{d}" -- 8835
  IO.println s!"{e}" -- 8835
  IO.println s!"{f}" -- 8835

I expected that calling randNat successively would produce different numbers, but it instead produces the same number, 8835. As far as I can tell, randNat returns the same generator it received. A little experimentation shows that when stdNext is passed default, we get default back, which I believe is the culprit here:

Lean 4 Web example

#eval do
  let gen : StdGen := default
  let (_, gen') := stdNext gen
  if gen.s1 ≠ gen'.s1 ∨ gen.s2 ≠ gen'.s2 then
    return "Recieved a different generator"
  return s!"Received the same generator"

(this evaluates to "Received the same generator")

Here's a better proof:
Lean 4 Web example

theorem instInhabitedStdGen.not_very_random : (stdNext default).snd = default := by
  simp [stdNext, instInhabitedStdGen]

[Aaron Liu]

The default StdGen is ⟨0, 0⟩

[Kyle Miller]

Looking at mkStdGen, it suggests that the generator should have nonzero state, but default sets the state to 0.

[Aaron Liu]

you should input a random generator instead

[Kyle Miller]

How about as a workaround, use mkStdGen?

I'm not sure that the Inhabited instance is meant to be the way you create generators (but I don't know that it's not)

[Kyle Miller]

Are you using default intentionally, or is default being used because of something else, like a derived Inhabited instance?

[Michael MacLeod]

Yes, the problem is what Aaron said about ⟨0, 0⟩ returning itself when passed to stdNext. If you use mkStdGen then this avoids the issue.

I was using it intentionally to test some code out I was working on. I just expected that the default instance of a random number generator would actually function as a random number generator, not a constant number generator. (is there a good reason to have the default instance be ⟨0, 0⟩?) I get that zero is a nice value to use as a default, but using it breaks the randomness.

[Robin Arnez]

It's even explicitly defined!

instance : Inhabited StdGen := ⟨{ s1 := 0, s2 := 0 }⟩

Changing this to

instance : Inhabited StdGen := ⟨{ s1 := 1, s2 := 1 }⟩

would probably fix the problems.

[Robin Arnez]

lean4#9782