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

• RandT and RandGT monad transformers for computations guided by randomness;
• Rand and RandG monads as special cases of the above
• 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 any monad that has access to stdGenRef.

References

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

@[inline, reducible]

abbrev RandGT (g : Type) (m : Type u_1 → Type u_2) (α : Type u_1) : Type (max u_1 u_2)

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

Equations

• RandGT g = StateT (ULift.{u_1, 0} g)

@[inline, reducible]

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

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

Equations

• RandG g = RandGT g Id

@[inline, reducible]

abbrev RandT (m : Type u_1 → Type u_2) (α : Type u_1) : Type (max u_1 u_2)

A monad transformer to generate random objects using the generator type StdGen. RandT m α should be thought of a random value in m α.

Equations

• RandT = RandGT StdGen

@[inline, reducible]

abbrev Rand (α : Type u_1) : Type u_1

A monad to generate random objects using the generator type StdGen.

Equations

• Rand = RandG StdGen

instance instMonadLiftTRandGTRandGT {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {g : Type} [MonadLift m n] : MonadLiftT (RandGT g m) (RandGT g n)

Equations

• instMonadLiftTRandGTRandGT = { monadLift := fun {α : Type u_1} (x : RandGT g m α) (s : ULift.{u_1, 0} g) => liftM (x s) }

class Random (m : Type u → Type u_1) (α : Type u) : Type (max (max 1 u) u_1)

Random m α gives us machinery to generate values of type α in the monad m.

Note that m is a parameter as some types may only be sampleable with access to a certain monad.

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

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

BoundedRandom m α gives us machinery to generate values of type α between certain bounds in the monad m.

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

def Rand.next {g : Type} {m : Type → Type u_1} [RandomGen g] [Monad m] : RandGT g m ℕ

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 {m : Type → Type u_1} {g : Type} [RandomGen g] [Monad m] : RandGT g m 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 {m : Type → Type u_1} {g : Type} [RandomGen g] [Monad m] : RandGT g m (ℕ × ℕ)

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 {m : Type u → Type u_1} {g : Type} (α : Type u) [Random m α] [RandomGen g] : RandGT g m α

Generate a random value of type α.

Equations

• Random.rand α = Random.random

def Random.randBound {m : Type u → Type u_1} {g : Type} (α : Type u) [Preorder α] [BoundedRandom m α] (lo : α) (hi : α) (h : lo ≤ hi) [RandomGen g] : RandGT g m { 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 {m : Type → Type u_1} [Monad m] {g : Type} {n : ℕ} [RandomGen g] : RandGT g m (Fin (Nat.succ n))

Equations

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

instance Random.instRandomFinSucc {m : Type → Type u_1} [Monad m] {n : ℕ} : Random m (Fin (Nat.succ n))

Equations

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

def Random.randBool {m : Type → Type u_1} [Monad m] {g : Type} [RandomGen g] : RandGT g m Bool

Equations

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

instance Random.instRandomBool {m : Type → Type u_1} [Monad m] : Random m Bool

Equations

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

instance Random.instRandomULift {m : Type u → Type u_1} {m' : Type (max v u) → Type u_2} {α : Type u} [ULiftable m m'] [Random m α] : Random m' (ULift.{v, u} α)

Equations

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

instance Random.instBoundedRandomNatToPreorderToPartialOrderStrictOrderedSemiring {m : Type → Type u_1} [Monad m] : BoundedRandom m ℕ

Equations

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

instance Random.instBoundedRandomIntToPreorderToPartialOrderToSemilatticeInfInstLatticeInt {m : Type → Type u_1} [Monad m] : BoundedRandom m ℤ

Equations

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

instance Random.instBoundedRandomFinToPreorderInstPartialOrderFin {m : Type → Type u_1} [Monad m] {n : ℕ} : BoundedRandom m (Fin n)

Equations

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

instance Random.instBoundedRandomULiftInstPreorderULift {m : Type u → Type u_1} {m' : Type (max v u) → Type u_2} {α : Type u} [Preorder α] [ULiftable m m'] [BoundedRandom m α] [Monad m'] : BoundedRandom m' (ULift.{v, u} α)

Equations

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

def IO.runRand {m : Type u_1 → Type u_2} {m₀ : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m₀] [ULiftable m₀ m] {α : Type u_1} (cmd : RandT m α) : m α

Computes a RandT m α 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 {m : Type u_1 → Type u_2} [Monad m] {α : Type u_1} (seed : ℕ) (cmd : RandT m α) : m α

Equations

• IO.runRandWith seed cmd = do let __do_lift ← StateT.run cmd { down := mkStdGen seed } pure __do_lift.1