Idris2Doc : System.Random.Pure

System.Random.Pure

(source)

Definitions

interface RandomGen : Type -> Type
  Interface of algorithms of pseudo-random generation of `Bits64` values using a seed type `g`.

Those `Bits64` values must be generated uniformly.
Splitting must give independent seeds.

Parameters: g
Methods:
next : g -> (g, Bits64)
split : g -> (g, g)
variant : Nat -> g -> g

Implementation: 
RandomGen StdGen
next : RandomGen g => g -> (g, Bits64)
Totality: total
Visibility: public export
split : RandomGen g => g -> (g, g)
Totality: total
Visibility: public export
variant : RandomGen g => Nat -> g -> g
Totality: total
Visibility: public export
splitStream : RandomGen g => g -> Stream g
  Stream of independent seeds

Totality: total
Visibility: public export
interface CanInitSeed : Type -> (Type -> Type) -> Type
  Interface for getting the starting seed

Parameters: g, m
Constraints: RandomGen g
Methods:
initSeed : m g
initSeed : CanInitSeed g m => m g
Totality: total
Visibility: public export
ConstSeed : Applicative m => RandomGen g => g -> CanInitSeed g m
Totality: total
Visibility: export
theSplitStream : CanInitSeed g m => Functor m => m (Stream g)
  Stream of independent seeds in the current context of `CanInitSeed`

Totality: total
Visibility: public export
interface Random : Type -> Type
  Interface for generation of values of particular types using any appropriate `RandomGen` algorithm.

Contains a function for generation of uniform value sitting in the given range,
and a function for generation of any value of the type.
For inifinite types, when no range is given, implementation determines actual used range by itself.

Parameters: a
Methods:
randomR : RandomGen g => (a, a) -> g -> (g, a)
random : RandomGen g => g -> (g, a)

Implementations:
Random Bits64
Random Int64
Random Bits32
Random Int32
Random Bits16
Random Int16
Random Bits8
Random Int8
Random Int
Random Integer
Random Nat
Random Double
Random ()
Random (Fin (S n))
Random Bool
Random Char
randomR : Random a => RandomGen g => (a, a) -> g -> (g, a)
Totality: total
Visibility: public export
random : Random a => RandomGen g => g -> (g, a)
Totality: total
Visibility: public export
randomFor : RandomGen g => (0 a : Type) -> Random a => g -> (g, a)
Totality: total
Visibility: public export
randomR' : Random a => RandomGen g => MonadState g m => (a, a) -> m a
Totality: total
Visibility: export
random' : Random a => RandomGen g => MonadState g m => m a
Totality: total
Visibility: export
randomFor' : RandomGen g => MonadState g m => (0 a : Type) -> Random a => m a
Totality: total
Visibility: public export
randomThru : (0 thru : Type) -> Random thru => (thru -> a) -> (a -> thru) -> Random a
Totality: total
Visibility: export
RandomInt64 : Random Int64
Totality: total
Visibility: export
RandomBits32 : Random Bits32
Totality: total
Visibility: export
RandomInt32 : Random Int32
Totality: total
Visibility: export
RandomBits16 : Random Bits16
Totality: total
Visibility: export
RandomInt16 : Random Int16
Totality: total
Visibility: export
RandomBits8 : Random Bits8
Totality: total
Visibility: export
RandomInt8 : Random Int8
Totality: total
Visibility: export
RandomInt : Random Int
Totality: total
Visibility: export
RandomNat : Random Nat
Totality: total
Visibility: export
RandomBool : Random Bool
Totality: total
Visibility: export