std.random

Random numbers, pure: a generator is a value, Random, and each draw gives what it drew and the generator to draw the next from — the same generator always draws the same. The generator is xoshiro256** (Blackman and Vigna), its state four 64-bit words, seeded, as its authors advise, by SplitMix64. It is no cryptographic generator: what it draws can be foretold from what it drew. Import it by a name, import std.random as Random, as the prelude has a split.

import std.random as Random

-- | a die thrown `n` times from the seed 7, the throws first first
-- | >>> throws 5
-- | [5, 2, 6, 6, 6]
throws : Int -> List Int
throws n = thrown n (Random.seeded 7) Nil
  where
  thrown : Int -> Random.Random -> List Int -> List Int
  thrown k r acc =
    if k <= 0 then List.reverse acc
    else (case Random.between r 1 6 of
          (x, next) -> thrown (k - 1) next (Cons x acc))

Random

data Random

A generator: xoshiro256**‘s state, four words, never all 0.

next

next : Random -> (UInt64, Random)

The generator’s next output, all 64 bits, and the generator after it. From the state 1, 2, 3, 4, the outputs of its authors’ code:

>>> List.map UInt64.toInt (draws next 4 (MkRandom 1 2 3 4))
[11520, 0, 1509978240, 1215971899390074240]

seeded

seeded : Int -> Random

The generator seeded by n: its four words SplitMix64’s first four outputs from the counter n, n taken modulo 2^64 (as UInt64.fromInt takes it: -1 is 2^64 - 1, and 2^64 is 0). From 0, they are the outputs SplitMix64’s authors give, 0xe220a8397b1dcdaf, 0x6e789e6aa1b965f4, 0x06c45d188009454f and 0xf88bb8a8724c81ec.

>>> seeded 0
MkRandom 16294208416658607535 7960286522194355700 487617019471545679 17909611376780542444
>>> draws next 3 (seeded 42)
[1546998764402558742, 6990951692964543102, 12544586762248559009]
>>> List.map (\n -> draws next 1 (seeded n)) [-1, 18446744073709551615, 18446744073709551616, 0]
[[10328197420357168392], [10328197420357168392], [11091344671253066420], [11091344671253066420]]

split

split : Random -> (Random, Random)

Two generators from one, to draw from apart: the first is the one after four outputs, the second is seeded by them, each mixed by SplitMix64 (so that its words are not outputs the first drew) — as seeded is, but from 256 bits, not 64. (Were all four 0, the second would be seeded 0.)

>>> draws next 2 (fst (split (seeded 0)))
[13521403990117723737, 18442103541295991498]
>>> draws next 2 (snd (split (seeded 0)))
[4854737294095960316, 9524419330683365375]

below

below : Random -> (bound : Int) -> (Int, Random)

An integer from 0 up to bound, bound not among them, each as likely as the others; bound at most 0, abandoned (as Go’s rand.IntN panics). A bound up to 2^32 takes Lemire’s way, the top 32 bits of an output times the bound, the high half of the product its answer — an output thrown away only where the low half falls in the few that would make some answers likelier. A greater bound (however great: an Int has no bound) takes as many outputs as it needs as one number, thrown away where it falls past the greatest multiple of the bound below the numbers they can make (fewer than half of them), and its remainder.

>>> draws (\r -> below r 10) 12 (seeded 1)
[7, 5, 5, 3, 6, 1, 0, 3, 8, 5, 9, 9]
>>> List.all (\x -> 0 <= x && x < 7) (draws (\r -> below r 7) 10000 (seeded 2))
True
>>> List.map (\v -> List.count (\x -> x == v) (draws (\r -> below r 3) 3000 (seeded 3))) [0, 1, 2]
[992, 984, 1024]
>>> draws (\r -> below r 1) 3 (seeded 4)
[0, 0, 0]
>>> List.all (\x -> 0 <= x && x < 4294967296) (draws (\r -> below r 4294967296) 1000 (seeded 5))
True

(bounds past 2^64: every draw below, and most of them past 2^64)

>>> List.all (\x -> 0 <= x && x < 1267650600228229401496703205376) (draws (\r -> below r 1267650600228229401496703205376) 1000 (seeded 6))
True
>>> List.count (\x -> x >= 18446744073709551616) (draws (\r -> below r 1267650600228229401496703205376) 1000 (seeded 6))
1000
>>> List.all (\x -> 0 <= x && x < 18446744073709551617) (draws (\r -> below r 18446744073709551617) 1000 (seeded 7))
True

between

between : Random -> Int -> Int -> (Int, Random)

An integer from lo to hi, both among them, each as likely as the others (below of how many there are, from lo); lo past hi, abandoned.

>>> draws (\r -> between r 1 6) 10 (seeded 8)
[5, 4, 4, 6, 3, 2, 3, 4, 6, 6]
>>> List.all (\x -> -3 <= x && x <= 3) (draws (\r -> between r (-3) 3) 1000 (seeded 9))
True
>>> draws (\r -> between r 5 5) 2 (seeded 10)
[5, 5]

float

float : Random -> (Float64, Random)

A float from 0 up to 1, 1 not among them: an output’s top 53 bits over 2^53, each of the 2^53 floats so made as likely as the others.

>>> List.all (\x -> 0.0 <= x && x < 1.0) (draws float 1000 (seeded 11))
True
>>> draws float 2 (seeded 0)
[0.6012629994179048, 0.7477740925472398]

shuffle

shuffle : {a : Type} -> Random -> List a -> (List a, Random)

The list in an order drawn, each of its orders as likely as the others: Fisher and Yates’s shuffle, in an array, from the last place down, each place’s element swapped with one drawn from it and those before it.

>>> fst (shuffle (seeded 12) ["a", "b", "c", "d", "e"])
["a", "e", "c", "d", "b"]
>>> List.sort (fst (shuffle (seeded 13) (List.range 1 100))) == List.range 1 100
True
>>> fst (shuffle (seeded 14) ([] : List Int))
[]

pick

pick : {a : Type} -> Random -> List a -> Maybe (a, Random)

An element of the list, each as likely as the others; of none, Nothing.

>>> maybe Nothing (\p -> (Just (fst p) : Maybe String)) (pick (seeded 15) ["x", "y", "z"])
Just "z"
>>> maybe Nothing (\p -> (Just (fst p) : Maybe String)) (pick (seeded 15) ([] : List String))
Nothing