# 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 #

@[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

Equations
Instances For
@[reducible, inline]
abbrev RandG (g : Type) (α : Type u_1) :
Type u_1

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

Equations
Instances For
@[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 α.

Equations
Instances For
@[reducible, inline]
abbrev Rand (α : Type u_1) :
Type u_1

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

Equations
Instances For
instance instMonadLiftTRandGTOfMonadLift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {g : Type} [] :
Equations
• instMonadLiftTRandGTOfMonadLift = { monadLift := fun {α : Type u_1} (x : RandGT g m α) (s : ) => 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 : ] → RandGT g m α
Instances
class BoundedRandom (m : Type u → Type u_1) (α : Type u) [] :
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 : ] → RandGT g m { a : α // lo a a hi }
Instances
def Rand.next {g : Type} {m : TypeType u_1} [] [] :

Generate one more Nat

Equations
• Rand.next = do let __do_liftget let rng : g := __do_lift.down match with | (res, new) => do set { down := new } pure res
Instances For
def Rand.split {m : TypeType u_1} {g : Type} [] [] :
RandGT g m g

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

Equations
• Rand.split = do let __do_liftget let rng : g := __do_lift.down match with | (r1, r2) => do set { down := r1 } pure r2
Instances For
def Rand.range {m : TypeType u_1} {g : Type} [] [] :
RandGT g m ()

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

Equations
• Rand.range = do let __do_liftget let rng : g := __do_lift.down pure ()
Instances For
def Random.rand {m : Type u → Type u_1} {g : Type} (α : Type u) [Random m α] [] :
RandGT g m α

Generate a random value of type α.

Equations
• = Random.random
Instances For
def Random.randBound {m : Type u → Type u_1} {g : Type} (α : Type u) [] [] (lo : α) (hi : α) (h : lo hi) [] :
RandGT g m { a : α // lo a a hi }

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

Equations
Instances For
def Random.randFin {m : TypeType u_1} [] {g : Type} {n : } [] :
RandGT g m (Fin n.succ)
Equations
Instances For
instance Random.instFinSucc {m : TypeType u_1} [] {n : } :
Random m (Fin n.succ)
Equations
• Random.instFinSucc = { random := fun {g : Type} [] => Random.randFin }
def Random.randBool {m : TypeType u_1} [] {g : Type} [] :
Equations
Instances For
instance Random.instBool {m : TypeType u_1} [] :
Equations
• Random.instBool = { random := fun {g : Type} [] => Random.randBool }
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' ()
Equations
• Random.instULiftOfULiftable = { random := fun {g : Type} [] => ULiftable.up Random.random }
instance Random.instBoundedRandomNat {m : TypeType u_1} [] :
Equations
• Random.instBoundedRandomNat = { randomR := fun {g : Type} (lo hi : ) (h : lo hi) (x : ) => do let zRandom.rand (Fin (hi - lo).succ) pure lo + z, }
instance Random.instBoundedRandomInt {m : TypeType u_1} [] :
Equations
• One or more equations did not get rendered due to their size.
instance Random.instBoundedRandomFin {m : TypeType u_1} [] {n : } :
Equations
• One or more equations did not get rendered due to their size.
instance Random.instBoundedRandomULiftOfULiftableOfMonad {m : Type u → Type u_1} {m' : Type (max v u) → Type u_2} {α : Type u} [] [ULiftable m m'] [] [Monad m'] :
Equations
• One or more equations did not get rendered due to their size.
def IO.runRand {m : Type u_1 → Type u_2} {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.
Instances For
def IO.runRandWith {m : Type u_1 → Type u_2} [] {α : Type u_1} (seed : ) (cmd : RandT m α) :
m α
Equations
Instances For