How to test Semigroup law for this data type?

568 views Asked by At

I'm trying to solve the same exercise as this other question in Chapter 15 of "Haskell Programming from First Principles". I've already made a Semigroup instance, and I'm having trouble writing the QuickCheck part of the exercise.

A Semigroup instance should satisfy:

a <> (b <> c) == (a <> b) <> c

where <> is the Semigroup mappend.

I have come up with the following:

import Data.Semigroup
import Test.QuickCheck

semigroupAssoc :: (Eq m, Semigroup m) => m -> m -> m -> Bool
semigroupAssoc a b c = (a <> (b <> c)) == ((a <> b) <> c)

newtype Combine a b = Combine { unCombine :: (a -> b) }

instance Semigroup b => Semigroup (Combine a b) where
  (Combine f) <> (Combine g) = Combine (\x -> (f x) <> (g x))

instance CoArbitrary (Combine a b) where
  coarbitrary (Combine f) = variant 0

instance (CoArbitrary a, Arbitrary b) => Arbitrary (Combine a b) where
  arbitrary = do
    f <- arbitrary
    return $ Combine f

type CombineAssoc a b = Combine a b -> Combine a b -> Combine a b -> Bool

main :: IO ()
main = do
  quickCheck (semigroupAssoc :: CombineAssoc Int Bool)

Everything compiles except for the quickCheck line, where it complains that there is No instance for (Eq (Combine Int Bool)) arising from a use of ‘semigroupAssoc’.

I don't think there is a way to test if two arbitrary function are equal (the functions wrapped up by Combine), but the exercise text suggests that such a thing is possible.

Any ideas on how I could make this work?

EDIT:

The authors give a hint for this exercise:

Hint: This function will eventually be applied to a single value of type a. But you’ll have multiple functions that can produce a value of type b. How do we combine multiple values so we have a single b? This one will probably be tricky! Remember that the type of the value inside of Combine is that of a function. If you can’t figure out CoArbitrary, don’t worry about QuickChecking this one.

@Li-yao Xia's answer seems to be the best answer. But shouldn't I use this CoArbitrary instance for something?

2

There are 2 answers

4
Li-yao Xia On BEST ANSWER

You can't decide whether two functions are equal. But you can test it!

Two functions are equal if and only if for any input they give the same output. This is a testable property: generate some inputs, compare the outputs. If they are different, you've got a counter-example.

-- Test.QuickCheck.(===) requires (Eq b, Show b)
-- but you can use (==) if you prefer.
funEquality :: (Arbitrary a, Show a, Eq b, Show b) => Combine a b -> Combine a b -> Property
funEquality (Combine f) (Combine g) =
  property $ \a -> f a === g a

Notice that the Bool result in the type of "decidable equality" (==) :: X -> X -> Bool is replaced with Property in what we might call "testable equality" funEquality :: X -> X -> Property. It's actually not necessary to use property and convert the function a -> Property (or a -> Bool if you use (==)) to Property, but the types look neater that way.

We need to rewrite the function corresponding to the associativity property, since we no longer rely on Eq.

type CombineAssoc a b = Combine a b -> Combine a b -> Combine a b -> Property

combineAssoc :: (Arbitrary a, Show a, Eq b, Show b, Semigroup b) => CombineAssoc a b
combineAssoc f g h = ((f <> g) <> h) `funEquality` (f <> (g <> h))

Edit: at this point we're actually still missing a Show instance for Combine. QuickCheck provides a wrapper Fun to both generate and show functions as counterexamples.

main = quickCheck $ \(Fn f) (Fn g) (Fn h) ->
  (combineAssoc :: CombineAssoc Int Bool) (Combine f) (Combine g) (Combine h)
0
leftaroundabout On

Indeed it is not possible or at least not feasible, however you don't really need a test case with such a big argument type as Int!

For smaller types, e.g. Int16, you can just exhaustively try all possible arguments to determine equality. The universe package has a convenient class for that:

import Data.Universe

instance (Universe a, Eq b) => Eq (Combine a b) where
  Combine f == Combine g = all (\x -> f x == g x) universe

Then your original check will work, albeit unacceptably slow; I'd recommend changing it to quickCheck (semigroupAssoc :: CombineAssoc Int16 Bool).