6.9. Random Numbers

🔗def
IO.setRandSeed (n : Nat) : BaseIO Unit
🔗def
IO.rand (lo hi : Nat) : BaseIO Nat
🔗def
randBool.{u} {gen : Type u} [RandomGen gen]
    (g : gen) : Bool × gen

Generate a random Boolean.

🔗def
randNat.{u} {gen : Type u} [RandomGen gen]
    (g : gen) (lo hi : Nat) : Nat × gen

Generate a random natural number in the interval [lo, hi].

6.9.1. Random Generators

🔗type class
RandomGen.{u} (g : Type u) : Type u

Interface for random number generators.

Instance Constructor

RandomGen.mk.{u} {g : Type u} (range : g → Nat × Nat) (next : g → Nat × g) (split : g → g × g) : RandomGen g

Methods

next:g → Nat × g

next operation returns a natural number that is uniformly distributed the range returned by range (including both end points), and a new generator.

range:g → Nat × Nat

range returns the range of values returned by the generator.

split:g → g × g

The 'split' operation allows one to obtain two distinct random number generators. This is very useful in functional programs (for example, when passing a random number generator down to recursive calls).

🔗structure
StdGen : Type

"Standard" random number generator.

Constructor

StdGen.mk (s1 s2 : Nat) : StdGen

Fields

s2:Nat
s1:Nat
🔗def
stdRange : Nat × Nat
🔗def
stdNext : StdGen → Nat × StdGen
🔗def
stdSplit : StdGen → StdGen × StdGen
🔗def
mkStdGen (s : Nat := 0) : StdGen

Return a standard number generator.

6.9.2. System Randomness

🔗
IO.getRandomBytes (nBytes : USize)
    : IO ByteArray

Read bytes from a system entropy source. Not guaranteed to be cryptographically secure. If nBytes = 0, return immediately with an empty buffer.