Haskell: Verify that every implementation for a function in a typeclass is commutative

user_15609870 0
Viewed 105

Suppose we have a function f :: (T a) => a -> a -> a -> in a typeclass T, typeclass which has instances in numerous types. Suppose we want this function to be commutative regardless of its implementation for a given type, i. e. ∀ a, b ∈ X: (T X, Eq X) => ∃ f X -> X -> X, f a b == f b a If I were to verify commutativity for a more concrete case, let`s say (+) and Int, I could write something like this:

import Test.Quickcheck (quickCheck)

commutativityProperty :: Eq a => (a -> a -> a) -> a -> a -> Bool
commutativityProperty f a b = f a b == f b a

main :: IO ()
main = do
  quickCheck (commutativityProperty (+) :: Int -> Int -> Bool)

quickCheck does not work with ambiguous type variables, so I could not write something like this: quickCheck (commutativityProperty (+) :: (Num a, Eq a) => a -> a -> Bool) Or, for the more general case: quickCheck (commutativityProperty f :: (T a, Eq a) => a -> a -> Bool) The Question is: In a similar context, where I know this function must hold commutativity regardless of implementation for a specific type, how can I verify that this is indeed true without having to write a line of quickCheck for every type that implements f and have to maintain that code (i.e. every time a new type with an instance of T is created, I would have to come back and write a new line for that specific type)?

testing properties haskell
2 Answers

Two approaches come to mind:

Generate random types

Using GADTs, you could try to generate a "random type" and use that for testing your polymorphic function. This is not entirely easy, but it could be still feasible depending on your typeclass.

To give you a very rough sketch:

data Ty t where
    TInt :: Ty Int
    TPair :: Ty a -> Ty b -> Ty (a,b)

data SomeType where
    ST :: Ty t -> SomeType

test :: SomeType -> (forall a . (T a) => a -> a -> a) -> Bool
test (ST TInt) f = f 4 2  -- actually, these should be generated randomly
test (ST (TPair x y)) f = ...

Testing non-integer types might come for free!

Every time we have a (terminating) polymorphic function, we know it satisfies a property called free theorem (the slogan is "theorems for free!"). E.g. if we have f :: a->a it has to be the identity, while g :: a->a->a has to be \x y->x or \x y->y. Adding a typeclass constraint like your T a makes it more complex, but a free theorem can still be generated.

It is likely that, using such a free theorem, you can prove that if your property hold for integers it has to hold for any type in class T. I'll give you an example.

Assume f :: Ord a => [a] -> [a] correctly sorts integers. Then, by the free theorem, it also sorts any other totally ordered type. Intuitively, this is because f can not really inspect the elements of the input list except using comparisons (<, compare,...). Hence, if you replace the list elements with suitable integers that have exactly the same comparison results, f must perform the "same" operation on both lists.

It is possible that you can play the same trick depending on what your T class actually allows.

user_32349590

The typeclass comes with a set of laws which should be fulfilled by each implementation. Whenever you add a new implementation you will have to add tests that make sure that your implementation is correct.

For writing those tests easier you may use libraries like https://hackage.haskell.org/package/quickcheck-classes but, eventually, you will have to write some code that tests the laws of typeclass against your implementation.

user_15939860
Related