The type T is not searchable¶
When writing a property using a forall
, we are
only allowed to use types which are searchable, that is, types for
which we can effectively generate sample values. Note this is not the
same thing as being finite. For example, the type of natural numbers
is searchable even though it is infinite; we can list natural numbers
(either in order or randomly) in order to see which ones make the
property true or false.
Disco> :test forall x:N. x < 10 -- this works as expected
- Test is false: ∀x. x < 10
Counterexample:
x = 10
On the other hand, the function type N -> N is not searchable: there is no way to list all functions of type N -> N. The below property is in fact false, but Disco can’t handle it:
Disco> :test forall f : N -> N. f(4) > 6
Error: the type
ℕ → ℕ
is not searchable (i.e. it cannot be used in a forall).
This error can also occur when you forget to put a type on a variable
in a forall
. For example:
Disco> :test forall x. x == x
Error: the type
a1
is not searchable (i.e. it cannot be used in a forall).
The problem here is really that Disco does not know what type x
should be. If we add a type annotation on x
, it works fine:
Disco> :test forall x: Bool. x == x
- Test passed: ∀x. x == x
No counterexamples exist.
Disco> :test forall x: N. x == x
- Test passed: ∀x. x == x
Checked 100 possibilities without finding a counterexample.