Quickcheck

Property testing: run a boolean property over many generated inputs and report the first counterexample, deterministically.

A Gen(a) is a seeded, sized function producing an a. It draws its randomness from the ambient Random effect, and the runner discharges that effect with a seeded SplitMix64 handler, so a whole run is a pure function of its seed. There is no real IO here: quickcheck performs no prim_rand, only the seeded stream, so a property that fails fails the same way on every backend and reruns identically from the reported seed. Determinism is the language’s contract, and a flaky property test would violate it.

The generator TYPE and its combinators live here; a derived Arbitrary(a) class (see Wire/deriving) supplies arbitrary : Gen(a) for user types by composing these combinators, so a derived instance plugs in with no rework.

Shrinking is intentionally omitted. The seam is the seed and size carried on a failing Outcome: a counterexample reproduces exactly via gen_at, and a future shrink : (a) -> List(a) hook would thread through check_go without changing this surface.

Types

Gen

type Gen(a) = Gen((Int) -> a ! {Random})

A seeded, sized generator of a. Apply it with gen_run; build one with the combinators below. The size bounds recursive shapes (list length, tree depth); make it explicit so derived instances for recursive types stay finite.

Config

type Config = Cfg { seed: U64, count: Int, max_size: Int }

How a property run configures the seeded stream: the base seed, the number of cases to try (count), and the largest size handed to a generator (max_size).

Outcome

type Outcome(a) = Passed(Int) | Failed(a, Int, U64, Int)

The result of a property run: Passed(n) after n cases held, or Failed(value, index, seed, size) with the first counterexample and the seed and size that reproduce it via gen_at.

Functions and Values

run_seeded

run_seeded : forall e0 a. (U64, () -> a ! {Random, e0}) -> a ! {e0}

Run action with the Random effect served by a seeded SplitMix64 stream, so the result is a pure function of seed. This is the REPLAYABLE handler the runner installs; call it directly to reproduce a single draw off a seed.

run_seeded(1u64, \() -> gen_run(gen_int, 5))

1

gen_run

gen_run : forall a. (Quickcheck.Gen(a), Int) -> a ! {Random}

Draw one value from g at the given size, performing Random. Discharge the Random with run_seeded (or use gen_at) to run it.

run_seeded(1u64, \() -> gen_run(gen_const(9), 5))

9

gen_at

gen_at : forall a. (Quickcheck.Gen(a), U64, Int) -> a

Draw a value from g deterministically off seed at size, no IO. This is the reproduce-a-counterexample entry point.

gen_at(gen_int, 42u64, 10)

-6

gen_const

gen_const : forall a. (a) -> Quickcheck.Gen(a)

The generator that ignores size and randomness and always yields x.

gen_at(gen_const(7), 1u64, 5)

7

gen_map

gen_map : forall a b. ((a) -> b, Quickcheck.Gen(a)) -> Quickcheck.Gen(b)

Map f over every value a generator produces.

gen_at(gen_map(\(x) -> x + 1, gen_const(4)), 1u64, 5)

5

gen_map2

gen_map2 : forall a b c. ((a, b) -> c, Quickcheck.Gen(a), Quickcheck.Gen(b)) -> Quickcheck.Gen(c)

Combine two generators with f, drawing both at the same size.

gen_at(gen_map2(\(a, b) -> a + b, gen_const(2), gen_const(3)), 1u64, 5)

5

gen_bind

gen_bind : forall a b. (Quickcheck.Gen(a), (a) -> Quickcheck.Gen(b)) -> Quickcheck.Gen(b)

Monadic bind: draw an a, then draw from the generator f picks for it.

gen_at(gen_bind(gen_const(3), \(x) -> gen_const(x * 2)), 1u64, 5)

6

gen_sized

gen_sized : forall a. ((Int) -> Quickcheck.Gen(a)) -> Quickcheck.Gen(a)

Build a generator that sees the current size, for recursive shapes that branch on remaining fuel.

gen_at(gen_sized(\(sz) -> gen_const(sz)), 1u64, 12)

12

gen_resize

gen_resize : forall a. (Int, Quickcheck.Gen(a)) -> Quickcheck.Gen(a)

Run g at a fixed size, ignoring the ambient one (shrink a recursive position by resizing it smaller).

gen_at(gen_resize(4, gen_sized(\(sz) -> gen_const(sz))), 1u64, 99)

4

gen_choose

gen_choose : forall a. (Quickcheck.Gen(a), List(Quickcheck.Gen(a))) -> Quickcheck.Gen(a)

Pick one of g0/rest uniformly, then draw from it (one arm per constructor, the shape a derived sum-type instance uses).

gen_at(gen_choose(gen_const(1), [gen_const(2)]), 5u64, 3)

1

gen_one_of

gen_one_of : forall a. (a, List(a)) -> Quickcheck.Gen(a)

Pick one of the given values uniformly (x0 or one of rest).

gen_at(gen_one_of(10, [20, 30]), 5u64, 3)

30

gen_int

gen_int : Quickcheck.Gen(Int)

Generator of Int, biased toward the edge cases (0, 1, -1, and a full-width draw) alongside small readable values.

gen_at(gen_int, 42u64, 10)

-6

gen_i64

gen_i64 : Quickcheck.Gen(I64)

Generator of I64, reusing the Int distribution.

gen_u64

gen_u64 : Quickcheck.Gen(U64)

Generator of U64, reusing the Int distribution (negatives wrap).

gen_bool

gen_bool : Quickcheck.Gen(Bool)

Generator of Bool.

gen_at(gen_bool, 7u64, 3)

false

gen_float

gen_float : Quickcheck.Gen(Float)

Generator of Float, including the nasty values (+/-0, +/-inf, NaN).

gen_char

gen_char : Quickcheck.Gen(Char)

Generator of a printable-ASCII Char.

gen_string

gen_string : Quickcheck.Gen(String)

Generator of a printable-ASCII String, length bounded by size.

gen_list

gen_list : forall a. (Quickcheck.Gen(a)) -> Quickcheck.Gen(List(a))

Generator of a List(a) whose length is bounded by size.

gen_at(gen_list(gen_const(1)), 7u64, 4)

[1, 1]

gen_option

gen_option : forall a. (Quickcheck.Gen(a)) -> Quickcheck.Gen(Option(a))

Generator of Option(a): None a quarter of the time, else Some.

gen_at(gen_option(gen_const(5)), 3u64, 3)

Some(5)

gen_pair

gen_pair : forall a b. (Quickcheck.Gen(a), Quickcheck.Gen(b)) -> Quickcheck.Gen((a, b))

Generator of a pair, both drawn at the same size.

gen_at(gen_pair(gen_const(1), gen_const(2)), 1u64, 3)

(1, 2)

gen_triple

gen_triple : forall a b c. (Quickcheck.Gen(a), Quickcheck.Gen(b), Quickcheck.Gen(c)) -> Quickcheck.Gen((a, b, c))

Generator of a triple, all drawn at the same size.

gen_at(gen_triple(gen_const(1), gen_const(2), gen_const(3)), 1u64, 3)

(1, 2, 3)

default_config

default_config : Quickcheck.Config

The default configuration: a fixed base seed, 100 cases, sizes up to 20.

default_config.count

100

check_with

check_with : forall a. (Quickcheck.Config, Quickcheck.Gen(a), (a) -> Bool) -> Quickcheck.Outcome(a)

Run prop over cfg.count inputs from gen, returning the first counterexample or the count that passed. Deterministic in cfg.seed.

check_with(default_config, gen_const(2), \(x) -> x == 2)

Quickcheck.Passed(100)

quickcheck

quickcheck : forall a. (Quickcheck.Gen(a), (a) -> Bool) -> Quickcheck.Outcome(a)

Run prop over the default configuration.

quickcheck(gen_int, \(x) -> x + 0 == x)

Quickcheck.Passed(100)

passed

passed : forall a. (Quickcheck.Outcome(a)) -> Bool

True when a run found no counterexample.

passed(quickcheck(gen_int, \(x) -> x + 1 > x))

true

show_outcome

show_outcome : forall a. (String, Quickcheck.Outcome(a)) -> String

Render an outcome for name as one report line (pass) or a block naming the counterexample and the seed and size that reproduce it.

show_outcome("positivity", Failed(0, 12, 42u64, 5))

positivity: FAILED after 12 tests.
  counterexample: 0
  reproduce: seed 42 size 5