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;
• 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 Plausible.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 Plausible.RandG (g : Type) (α : Type u_1) : Type u_1

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

@[reducible, inline]

abbrev Plausible.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 Plausible.Rand (α : Type u_1) : Type u_1

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

@[implicit_reducible]

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

  Generate a value of type α randomly using generator g.

class Plausible.BoundedRandom (m : Type u → Type u_1) (α : Type u) [LE α] : 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 }

  Generate a value of type α between lo and hi randomly using generator g.

@[inline]

def Plausible.RandT.up {α : Type u} {m : Type u → Type w} {m' : Type (max u v) → Type w'} {g : Type} [RandomGen g] [Monad m] [Monad m'] (m_up : {α : Type u} → m α → m' (ULift α)) (x : RandGT g m α) : RandGT g m' (ULift α)

Given a random generator for α, we can convert it to a random generator for ULift α.

@[inline]

def Plausible.RandT.down {α : Type u} {m : Type (max u v) → Type w} {m' : Type u → Type w'} {g : Type} [RandomGen g] [Monad m] [Monad m'] (m_down : {α : Type u} → m (ULift α) → m' α) (x : RandGT g m (ULift α)) : RandGT g m' α

Given a random generator for ULift α, we can convert it to a random generator for α.

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

Generate one more Nat

def Plausible.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 Plausible.Rand.range {m : Type → Type u_1} {g : Type} [RandomGen g] [Monad m] : RandGT g m (Nat × Nat)

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

@[inline]

def Plausible.Rand.up {α : Type u} {g : Type} [RandomGen g] (x : RandG g α) : RandG g (ULift α)

Given a random generator for α, we can convert it to a random generator for ULift α.

@[inline]

def Plausible.Rand.down {α : Type u} {g : Type} [RandomGen g] (x : RandG g (ULift α)) : RandG g α

Given a random generator for ULift α, we can convert it to a random generator for α.

def Plausible.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 Plausible.Random.randBound {m : Type u → Type u_1} {g : Type} (α : Type u) [LE α] [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 Plausible.Random.randFin {m : Type → Type u_1} [Monad m] {g : Type} {n : Nat} [RandomGen g] : RandGT g m (Fin n.succ)

Generate a random Fin.

@[implicit_reducible]

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

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

Generate a random Bool.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Plausible.Random.instBoundedRandomBitVec {m : Type → Type u_1} [Monad m] {n : Nat} : BoundedRandom m (BitVec n)

def Plausible.runRand {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] {α : Type} (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.

def Plausible.runRandWith {m : Type → Type u_1} [Monad m] {α : Type} (seed : Nat) (cmd : RandT m α) : m α

Run the random computation cmd with seed for the RNG.