Email Gateway (Aug 18 2022 at 18:22): Email Gateway (Aug 18 2022 at 18:22):From: Lukas Bulwahn <bulwahn@in.tum.de>
Hi Yuhui,
Quickcheck tries to execute this proposition using the code generation
facility.
The functions (alpha => bool) are translated to functions in ML.
To allow to check for function equality, it requires that the type of
the domain is finite (and enumerable, being of type class enum).
For the obvious finite types (unit and bool), we provide instantiations.
To polymorphic types, we check with small finite types that are of class
enum.
Infinite types, such as int and nat, are not enumerable, and we cannot
check for function equality (for the chosen translation above).
The solution to enable execution of this proposition even with an
infinite type is to choose a different representation for functions (and
sets).
Different on-going discussions and effort by the developers will soon
enable that this is possible, but right now, we are at the unlucky stage
that none of them are fully automatic and could be applied by quickcheck
behind the scenes.
NB: I am still not happy with the error message. It is the honest truth,
why quickcheck cannot execute the proposition, but admittedly users
might struggle understanding its explanation.
Lukas
Last updated: Nov 21 2024 at 12:39 UTC