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