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

@[reducible, inline]

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

@[reducible, inline]

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

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

@[reducible, inline]

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 α.

@[reducible, inline]

abbrev Rand (α : Type u_1) : Type u_1

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

@[implicit_reducible]

instance instMonadLiftTRandGTOfMonadLift {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)

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} [RandomGen g] : RandGT g m α

  Sample an element of this type from the provided generator.

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 : α) (h : lo ≤ hi) [RandomGen g] : RandGT g m { a : α // lo ≤ a ∧ a ≤ hi }

  Sample a bounded element of this type from the provided generator.

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

Generate a random Nat.

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.

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.

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 α.

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.

def Random.randFin {m : Type → Type u_1} [Monad m] {g : Type} {n : ℕ} [NeZero n] [RandomGen g] : RandGT g m (Fin n)

Generate a random Fin.

@[implicit_reducible]

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

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

Generate a random Bool.

@[implicit_reducible]

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

@[implicit_reducible]

instance Random.instULiftOfULiftable {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} α)

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Random.instBoundedRandomULiftOfULiftableOfMonad {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} α)

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

Execute 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.

def IO.runRandWith {m : Type u_1 → Type u_2} [Monad m] {α : Type u_1} (seed : ℕ) (cmd : RandT m α) : m α

Execute RandT m α using the global stdGenRef as RNG and the given seed.