multicoretests
multicoretests copied to clipboard
Specifications can be terser through more type trickery
As I was writing an STM specification for Dynarrays, I was a bit frustrated to have to add a catch-all assert false
at the end of postcond
. So I went into an over-engineering rabbit hole and found that it can be avoided by making the cmd
type of specifications a GADT, which allows to specify the result type for commands. The typechecker is then able to deduce the result type when pattern matching on commands.
As an example, I have rewritten src/atomic/stm_tests.ml
to match the new Spec
signature.
This has a number of benefits and some drawbacks.
Benefits
- When writing the
run
function, results no longer need to be wrappend into theRes
constructor. However, it is still necessary to also return an instance of'a ty_show
; I have not found a simpler way to make the results printable. - When writing the
postcond
function, it is no longer necessary to match on patterns likeRes ((Result (Int, Exn), _), v)
for the typechecker to deduce the right type forv
: the command name suffices. It is also no longer necessary to add a catch-all_ -> assert false
at the end. - Functions like
run
are safer because the result type is checked.
Drawbacks
Defining a GADT in the specification adds its own boilerplate: most functions now need explicit type annotations with universal quantifiers; the user must also define an existential type packed_cmd
and wrap the command generators in it. Such STM tests are harder to write when one is not familiar with qcheck-stm.
And of course, another big drawback is that it changes the signature of STM specifications.
For these reasons, I open this PR as a draft, mostly to share the idea.