21.10. 随机数🔗

定义

IO.setRandSeed (n : Nat) : BaseIO Unit
IO.setRandSeed (n : Nat) : BaseIO Unit

为 IO.rand 所使用的随机数生成器状态设定种子。

定义

IO.rand (lo hi : Nat) : BaseIO Nat
IO.rand (lo hi : Nat) : BaseIO Nat

返回 lo 与 hi 之间的一个伪随机数，并使用、更新一个已保存的随机数生成器状态。

该状态可通过 IO.setRandSeed 设定种子。

定义

randBool.{u} {gen : Type u} [RandomGen gen] (g : gen) : Bool × gen
randBool.{u} {gen : Type u}
  [RandomGen gen] (g : gen) : Bool × gen

生成一个随机布尔值。

定义

randNat.{u} {gen : Type u} [RandomGen gen] (g : gen) (lo hi : Nat) :
  Nat × gen
randNat.{u} {gen : Type u} [RandomGen gen]
  (g : gen) (lo hi : Nat) : Nat × gen

在区间 [lo, hi] 内生成一个随机自然数。

21.10.1. 随机数生成器🔗

类型类

RandomGen.{u} (g : Type u) : Type u
RandomGen.{u} (g : Type u) : Type u

随机数生成器的接口。

实例构造子

RandomGen.mk.{u}

方法

range : g → Nat × Nat

range 返回该生成器会产生的值域。

next : g → Nat × g

next 操作返回一个在 range 所返回区间内（包含两个端点）均匀分布的自然数，以及一个新的生成器。

split : g → g × g

split 操作允许获得两个不同的随机数生成器。这在函数式程序中非常有用（例如将随机数生成器传递给递归调用时）。

结构体

StdGen : Type
StdGen : Type

“标准”随机数生成器。

定义

stdRange : Nat × Nat
stdRange : Nat × Nat

StdGen 返回值的范围。

定义

stdNext : StdGen → Nat × StdGen
stdNext : StdGen → Nat × StdGen

StdGen 的下一个值，以及更新后的生成器状态。

定义

stdSplit : StdGen → StdGen × StdGen
stdSplit : StdGen → StdGen × StdGen

将一个 StdGen 拆分为两个独立状态。

定义

mkStdGen (s : Nat := 0) : StdGen
mkStdGen (s : Nat := 0) : StdGen

返回一个标准随机数生成器。

21.10.2. 系统随机性🔗

不透明定义

IO.getRandomBytes (nBytes : USize) : IO ByteArray
IO.getRandomBytes (nBytes : USize) :
  IO ByteArray

从系统熵源中读取字节。它不保证具有密码学安全性。

如果 nBytes 为 0，则立即返回一个空缓冲区。