Documentation

Mathlib.Control.Random

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 #

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} [MonadLift m n] :
          Equations
          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.

          Instances
            class BoundedRandom (m : Type u → Type u_1) (α : Type u) [Preorder α] :
            Type (max (max 1 u) u_1)

            BoundedRandom m α gives us machinery to generate values of type α between certain bounds in the monad m.

            Instances
              def Rand.next {g : Type} {m : TypeType u_1} [RandomGen g] [Monad m] :

              Generate one more Nat

              Equations
              • Rand.next = do let __do_liftget let rng : g := __do_lift.down match RandomGen.next rng with | (res, new) => do set { down := new } pure res
              Instances For
                def Rand.split {m : TypeType 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
                • Rand.split = do let __do_liftget let rng : g := __do_lift.down match RandomGen.split rng with | (r1, r2) => do set { down := r1 } pure r2
                Instances For
                  def Rand.range {m : TypeType u_1} {g : Type} [RandomGen g] [Monad m] :

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

                  Equations
                  Instances For
                    def 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
                    Instances For
                      def Random.randBound {m : Type u → Type u_1} {g : Type} (α : Type u) [Preorder α] [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
                      Instances For
                        def Random.randFin {m : TypeType u_1} [Monad m] {g : Type} {n : } [RandomGen g] :
                        RandGT g m (Fin n.succ)
                        Equations
                        Instances For
                          instance Random.instFinSucc {m : TypeType u_1} [Monad m] {n : } :
                          Random m (Fin n.succ)
                          Equations
                          • Random.instFinSucc = { random := fun {g : Type} [RandomGen g] => Random.randFin }
                          def Random.randBool {m : TypeType u_1} [Monad m] {g : Type} [RandomGen g] :
                          Equations
                          Instances For
                            instance Random.instBool {m : TypeType u_1} [Monad m] :
                            Equations
                            • Random.instBool = { random := fun {g : Type} [RandomGen g] => 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 α] :
                            Equations
                            Equations
                            Equations
                            • One or more equations did not get rendered due to their size.
                            instance Random.instBoundedRandomFin {m : TypeType u_1} [Monad m] {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} [Preorder α] [ULiftable m m'] [BoundedRandom 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₀ : TypeType} [Monad m] [MonadLiftT (ST IO.RealWorld) 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} [Monad m] {α : Type u_1} (seed : ) (cmd : RandT m α) :
                              m α
                              Equations
                              Instances For