Rand Monad and Random Class

This module provides tools for formulating computations guided by randomness and for defining objects that can be created randomly.

Main definitions

• Rand and RandG monad for computations guided by randomness;
• Random class for objects that can be generated randomly;
  • random to generate one object;
• BoundedRandom class for objects that can be generated randomly inside a range;
  • randomR to generate one object inside a range;
• IO.runRand to run a randomized computation inside the IO monad;

References

• Similar library in Haskell: https://hackage.haskell.org/package/MonadRandom

@[inline, reducible]

abbrev RandG (g : Type) (α : Type u_1) : Type u_1

A monad to generate random objects using the generic generator type g

@[inline, reducible]

abbrev Rand (α : Type u) : Type u

A monad to generate random objects using the generator type Rng

class Random (α : Type u) : Type (max 1 u)

• random : {g : Type} → [inst : RandomGen g] → RandG g α

Random α gives us machinery to generate values of type α

class BoundedRandom (α : Type u) [Preorder α] : Type (max 1 u)

• randomR : {g : Type} → (lo hi : α) → lo ≤ hi → [inst : RandomGen g] → RandG g { a // lo ≤ a ∧ a ≤ hi }

BoundedRandom α gives us machinery to generate values of type α between certain bounds

def Rand.next {g : Type} [RandomGen g] : RandG g ℕ

Generate one more Nat

def Rand.split {g : Type} [RandomGen g] : RandG g g

Create a new random number generator distinct from the one stored in the state

def Rand.range {g : Type} [RandomGen g] : RandG g (ℕ × ℕ)

Get the range of Nat that can be generated by the generator g

def Random.rand {g : Type} (α : Type u) [Random α] [RandomGen g] : RandG g α

Generate a random value of type α.

def Random.randBound {g : Type} (α : Type u) [Preorder α] [BoundedRandom α] (lo : α) (hi : α) (h : lo ≤ hi) [RandomGen g] : RandG g { a // lo ≤ a ∧ a ≤ hi }

Generate a random value of type α between x and y inclusive.

def Random.randFin {g : Type} {n : ℕ} [RandomGen g] : RandG g (Fin (Nat.succ n))

instance Random.instRandomFinSucc {n : ℕ} : Random (Fin (Nat.succ n))

def Random.randBool {g : Type} [RandomGen g] : RandG g Bool

instance Random.instRandomBool : Random Bool

instance Random.instRandomULift {α : Type u} [Random α] : Random (ULift.{v, u} α)

instance Random.instBoundedRandomNatToPreorderToPartialOrderStrictOrderedSemiring : BoundedRandom ℕ

instance Random.instBoundedRandomIntToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeInstLinearOrderInt : BoundedRandom ℤ

instance Random.instBoundedRandomFinToPreorderInstPartialOrderFin {n : ℕ} : BoundedRandom (Fin n)

instance Random.instBoundedRandomULiftInstPreorderULift {α : Type u} [Preorder α] [BoundedRandom α] : BoundedRandom (ULift.{v, u} α)

def IO.runRand {α : Type} (cmd : Rand α) : BaseIO α

Computes a Rand α using the global stdGenRef as RNG. Note that:

• stdGenRef is not necessarily properly seeded on program startup as of now and will therefore be deterministic.
• stdGenRef is not thread local, hence two threads accessing it at the same time will get the exact same generator.

def IO.runRandWith {α : Type} (seed : ℕ) (cmd : Rand α) : BaseIO α