Search code examples
genericshaskellquickcheck

Proof/testing correctness of generic functions

(This is not about theorem proving is about testing in practice like quickCheck)

Let f some generic function

f :: RESTRICTIONS => GENERICS

with some "desirable" properties (i.e. is not a hack, is immutable, ...) typically a pure Haskell generic function.

Suppose we want test it, the main question is

if we have (well) tested that function for one specific type (e.g. Int), can we assume it is correct for all types? (matching restrictions, of course)

(with "well tested" I mean "all" function {domain X properties} have been tested)

Theorically we can be sure but, I'm not sure if some additional property, restriction, ... at instantiation process (i.e. compilation) maybe have influence.

Thanks!

NOTE tests maybe use certain type specific properties (e.g. Int) but these properties can not be part of tested properties. E.g. if Monoid is a restriction then, associativity can be part of tested properties (but not commutativity if is not a restriction).

EXAMPLE

let f

repeatedHeader :: Eq a => [a] -> Bool
repeatedHeader (x:y:_) = x == y
repeatedHeader _ = False

test1 = repeatedHeader [1,1,2] == True
test2 = repeatedHeader [1,2,3] == False
Solution

  • You can be sure only in the trivial case that RESTRICTIONS is empty or at least does not mention the generic type in question.

    In all other cases, your function depends on functionality of type class instances. But even if all existing instances behave the way you expect, this does not have to be true for the type class instance that is written tomorrow.

    So, it is a question of enforcing certain properties in instances. And this is generally a weak point, because type class laws are mostly stated informally only. For example, Haskell can't and won't prevent you from making a faulty Eq or Ord instance.

    A real world example would be a test of a function like:

    f :: Num a => a -> a

    Now, we know we do have types that overflow silently, like Int. Others don't. This is silently tolerated in the Num class, because, well, life is just like that. Hence, once you did all tests using Double you can still get surprised if you use f on Int.