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

• Rand and RandG monad for computations guided by randomness;
• 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 the IO monad;

References

• Similar library in Haskell: https://hackage.haskell.org/package/MonadRandom

ink

@[inline]

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

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

Equations

• RandG g = StateM (ULift g)

ink

@[inline]

abbrev Rand (α : Type u) : Type u

A monad to generate random objects using the generator type Rng

Equations

• Rand α = RandG StdGen α

ink

class Random (α : Type u) : Type (max1u)

• random : {g : Type} → [inst : RandomGen g] → RandG g α

Random α gives us machinery to generate values of type α

ink

class BoundedRandom (α : Type u) [inst : Preorder α] : Type (max1u)

• randomR : {g : Type} → (lo hi : α) → lo ≤ hi → [inst : RandomGen g] → RandG g { a // lo ≤ a ∧ a ≤ hi }

BoundedRandom α gives us machinery to generate values of type α between certain bounds

ink

def Rand.next {g : Type} [inst : RandomGen g] : RandG g ℕ

Generate one more Nat

Equations

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

ink

def Rand.split {g : Type} [inst : RandomGen g] : RandG g g

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

Equations

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

ink

def Rand.range {g : Type} [inst : RandomGen g] : RandG g (ℕ × ℕ)

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

Equations

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

ink

def Random.rand {g : Type} (α : Type u) [inst : Random α] [inst : RandomGen g] : RandG g α

Generate a random value of type α.

Equations

• Random.rand α = Random.random

ink

def Random.randBound {g : Type} (α : Type u) [inst : Preorder α] [inst : BoundedRandom α] (lo : α) (hi : α) (h : lo ≤ hi) [inst : RandomGen g] : RandG g { a // lo ≤ a ∧ a ≤ hi }

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

Equations

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

ink

def Random.randFin {g : Type} {n : ℕ} [inst : RandomGen g] : RandG g (Fin (Nat.succ n))

Equations

• Random.randFin x = match x with | { down := g } => Prod.map Fin.ofNat ULift.up (randNat g 0 (Nat.succ n))

ink

instance Random.instRandomFinSucc {n : ℕ} : Random (Fin (Nat.succ n))

Equations

• Random.instRandomFinSucc = { random := fun {g} [RandomGen g] => Random.randFin }

ink

def Random.randBool {g : Type} [inst : RandomGen g] : RandG g Bool

Equations

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

ink

instance Random.instRandomBool : Random Bool

Equations

• Random.instRandomBool = { random := fun {g} [RandomGen g] => Random.randBool }

ink

instance Random.instBoundedRandomNatToPreorderToPartialOrderStrictOrderedSemiring : BoundedRandom ℕ

Equations

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

ink

instance Random.instBoundedRandomIntToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeInstLinearOrderInt : BoundedRandom ℤ

Equations

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

ink

instance Random.instBoundedRandomFinToPreorderInstPartialOrderFin {n : ℕ} : BoundedRandom (Fin n)

Equations

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

ink

def IO.runRand {α : Type} (cmd : Rand α) : BaseIO α

Computes a Rand α 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.

ink

def IO.runRandWith {α : Type} (seed : ℕ) (cmd : Rand α) : BaseIO α

Equations

• IO.runRandWith seed cmd = pure (StateT.run cmd { down := mkStdGen seed }).fst