# 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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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.31} (x : Plausible.RandGT g m α) (s : ULift g) => liftM (x s) }

source
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`.

Instances

source
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`.

Instances

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

source
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)

Instances For

source
@[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.25} (x : Id α) => pure { down := x.run }) x

Instances For

source
@[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.25} (x : Id (ULift α)) => pure x.run.down) x

Instances For

source
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

Instances For

source
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

Instances For

source
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))

Instances For

source
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 }

source
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)

Instances For

source
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 }

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

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

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

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

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

Instances For

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

Run the random computaton `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

Instances For