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

Equations

• Plausible.RandGT g = StateT (ULift 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.

Equations

• Plausible.RandG g = Plausible.RandGT g Id

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

Equations

• Plausible.RandT = Plausible.RandGT StdGen

@[reducible, inline]

abbrev Plausible.Rand (α : Type u_1) : Type u_1

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

Equations

• Plausible.Rand = Plausible.RandG 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)

Equations

• Plausible.instMonadLiftTRandGTOfMonadLift = { monadLift := fun {α : Type ?u.32} (x : Plausible.RandGT g m α) (s : ULift g) => liftM (x s) }

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

Equations

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

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

Equations

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

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

Generate one more Nat

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Plausible.Rand.up x = Plausible.RandT.up (fun {α : Type ?u.26} (x : Id α) => pure { down := x.run }) x

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

Equations

• Plausible.Rand.down x = Plausible.RandT.down (fun {α : Type ?u.26} (x : Id (ULift α)) => pure x.run.down) x

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

Equations

• Plausible.Random.rand α = Plausible.Random.random

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.

Equations

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

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.

Equations

• Plausible.Random.randFin { down := g_1 } = pure (Prod.map (Fin.ofNat n.succ) ULift.up (randNat g_1 0 n))

@[implicit_reducible]

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

Equations

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

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

Generate a random Bool.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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.

Equations

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

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.

Equations

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