Expand description
One type-directed value generator, used by three features.
docs/21-tests-in-beck-and-proof.md §21.3 rule 5: “Stub return values, property-test inputs
and given gaps are the same problem: produce an inhabitant of a known type. The compiler has
the full type, including newtypes, unions and records, so it can derive:
- a canonical inhabitant (first variant, empty collection, zero,
"") for the don’t-care case; - an arbitrary one, with shrinking, for
propertyblocks; - and it can refuse, with a diagnostic, for a type with no inhabitant it can construct —
secret[T]being the interesting one, since inventing a secret in a test is exactly the sort of thing that should require somebody to type it out.“
“This is one generator, used by three features, and it is the piece to build first because §21.2’s property tests need it too.” It is built once, here.
§Determinism
The randomness is a counter-based splitmix, seeded from the test’s name and the run index — not from a clock. §21.2: “A flaky Beck test should be impossible, and if one appears it is a compiler defect.” A property test that fails on run 37 fails on run 37 again, on any machine, so the shrunk counterexample the report prints is one a person can reproduce by re-running the command they already ran.
Structs§
- Rng
- A counter-based PRNG. Splitmix64, which is the whole algorithm and needs no state beyond a counter — so a value’s generation depends on where it is asked for, and nothing else.
- Uninhabitable
- A type the generator will not invent a value for, and why.
Functions§
- arbitrary
- An arbitrary inhabitant, for a
propertyblock’s parameters. - canonical
- The don’t-care inhabitant — §21.3 rule 1’s “‘any value’ is the default, so it needs no expression”.
- shrink
- Smaller candidates for a failing input, most-shrunk first.
- size
- A total order on “how big is this value”, used to prove a shrink is progress.