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

Equations

• RandG g = StateM (ULift.{u_1, 0} g)

@[inline, reducible]

abbrev Rand (α : Type u) : Type u

A monad to generate random objects using the generator type Rng

Equations

• Rand α = RandG StdGen α

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

Equations

• Rand.next = do let __do_lift ← get let rng : g := __do_lift.down match RandomGen.next rng with | (res, new) => do set { down := new } pure res

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

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

Equations

• Rand.split = do let __do_lift ← get let rng : g := __do_lift.down match RandomGen.split rng with | (r1, r2) => do set { down := r1 } pure r2

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

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

Equations

• Rand.range = do let __do_lift ← get let rng : g := __do_lift.down pure (RandomGen.range rng)

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

Generate a random value of type α.

Equations

• Random.rand α = Random.random

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.

Equations

• Random.randBound α lo hi h = BoundedRandom.randomR lo hi h

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

Equations

• Random.randFin x = match x with | { down := g } => Prod.map Fin.ofNat ULift.up (randNat g 0 (Nat.succ n))

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

Equations

• Random.instRandomFinSucc = { random := fun {g} [RandomGen g] => Random.randFin }

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

Equations

• Random.randBool = do let __do_lift ← Random.rand (Fin 2) pure (__do_lift == 1)

instance Random.instRandomBool : Random Bool

Equations

• Random.instRandomBool = { random := fun {g} [RandomGen g] => Random.randBool }

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

Equations

• Random.instRandomULift = { random := fun {g} [RandomGen g] => ULiftable.up Random.random }

instance Random.instBoundedRandomNatToPreorderToPartialOrderStrictOrderedSemiring : BoundedRandom ℕ

Equations

• One or more equations did not get rendered due to their size.

instance Random.instBoundedRandomIntToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeInstLinearOrderInt : BoundedRandom ℤ

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• IO.runRandWith seed cmd = pure (StateT.run cmd { down := mkStdGen seed }).fst