Documentation

Plausible.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 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
    Instances For
      @[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
        Instances For
          @[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
            Instances For
              @[reducible, inline]
              abbrev Plausible.Rand (α : Type u_1) :
              Type u_1

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

              Equations
                Instances For
                  instance Plausible.instMonadLiftTRandGTOfMonadLift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {g : Type} [MonadLift m n] :
                  Equations
                    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
                      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
                        @[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
                          Instances For
                            @[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
                              Instances For
                                def Plausible.Rand.next {g : Type} {m : TypeType u_1} [RandomGen g] [Monad m] :

                                Generate one more Nat

                                Equations
                                  Instances For
                                    def Plausible.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
                                      Instances For
                                        def Plausible.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
                                            @[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
                                              Instances For
                                                @[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
                                                  Instances 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 α.

                                                    Equations
                                                      Instances For
                                                        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
                                                          Instances For
                                                            def Plausible.Random.randFin {m : TypeType u_1} [Monad m] {g : Type} {n : Nat} [RandomGen g] :
                                                            RandGT g m (Fin n.succ)

                                                            Generate a random Fin.

                                                            Equations
                                                              Instances For
                                                                instance Plausible.Random.instFinSucc {m : TypeType u_1} [Monad m] {n : Nat} :
                                                                Equations
                                                                  def Plausible.Random.randBool {m : TypeType u_1} [Monad m] {g : Type} [RandomGen g] :

                                                                  Generate a random Bool.

                                                                  Equations
                                                                    Instances For
                                                                      instance Plausible.Random.instBool {m : TypeType u_1} [Monad m] :
                                                                      Equations
                                                                        instance Plausible.Random.instBoundedRandomFin {m : TypeType u_1} [Monad m] {n : Nat} :
                                                                        Equations
                                                                          Equations
                                                                            def Plausible.runRand {m : TypeType} [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
                                                                              Instances For
                                                                                def Plausible.runRandWith {m : TypeType u_1} [Monad m] {α : Type} (seed : Nat) (cmd : RandT m α) :
                                                                                m α

                                                                                Run the random computaton cmd with seed for the RNG.

                                                                                Equations
                                                                                  Instances For