[Haskell-cafe] property testing with context

[Ben Franksen]

Am 19.10.2018 um 22:53 schrieb Olaf Klinke:
> the solution might be simple: Don't express the property as an atomic
> function (a -> Bool). This reminds me a bit of the Cutty-Howard
> correspondence, only that proofs are replaced by counterexamples. A
> testing library should have an operator for each of the logical
> connectives, where
> 
> - a counterexample to True is never found
> - a counterexample to False is ()
> - a counterexample to (not x) is an example for x
> - a counterexample to (x && y) is either a counterexample to x or a counterexample to y, whichever is found first
> - a counterexample to (x || y) is a pair of counterexamples to both x and y
> - a counterexample to (x ==> y) is an example for x together with a counterexample for y
> 
> Then, if you build your property out of smaller properties and the connectives above, the counterexample-finder would be able to inform you which part of the property failed. I'm pretty sure at least one of the testing libraries has a system like this. 
> 

Hi Olaf

while this approach works in principle it has practical disadvantages.

One charming feature of property testing in Haskell is that expressing
properties does normally /not/ require to import the testing library.
This allows me to write my properties in a generic style that works with
e.g. quickcheck, leancheck, smallcheck etc. With your approach I would
be tied to a single property testing library.

I guess this would be less of a problem if in Haskell the boolean
operators were overloaded i.e. part of a class. I think this was an
oversight when the Prelude and the standard libraries were designed. IME
boolean algebras (or perhaps more generally lattices) appear
/everywhere/. I can't count the number of times I wanted to use these
operators on structures containing Bools or functions returning Bool and
couldn't. IMHO such a generalization would be a lot more useful and less
controversial than the one from List to Foldable.

(I can't remember a single instance where I missed this generalization
of lists. In fact I think is completely useless. Foldable essentially
allows me to say: "give me all your elements, one by one, in /your/
preferred order, so I can combine them to something new". Due to the
laziness of lists this is really the same as having a toList function
(modulo list fusion to take care of the constant factor overhead). Only
that a container type may offer many different versions of toList but
only a single Foldable instance. I understand that foldr and foldl have
been added to the class to allow at least two different "preferred"
traversal orders, but adding methods to a class in this way obviously
doesn't scale and is poor design, again IMHO.)

Cheers
Ben