haskellapplicativequickcheck

QuickCheck returns "0 tests" when checking Applicative homomorphism property (Binary Tree)


I would like to check that homomorphism Applicative law holds for datatype BinTree:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-} 
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}

module Laws where

import Control.Applicative ((<$>), liftA3)

import Data.Monoid

import Test.QuickCheck
import Test.QuickCheck.Function
import Test.QuickCheck.Gen

data BinTree a = Empty | Node a (BinTree a) (BinTree a) deriving (Show, Eq)

instance Functor BinTree where
    fmap _ Empty = Empty
    fmap f (Node x hi hd) = Node (f x) (fmap f hi) (fmap f hd)

instance Applicative BinTree where
    -- pure :: a -> BinTree a
    pure x = Node x (pure x) (pure x)

    -- <*> :: BinTree (a -> b) -> BinTree a -> BinTree b
    _ <*> Empty = Empty -- L1, 
    Empty <*> t = Empty
    (Node f l r) <*> (Node x l' r') = Node (f x) (l <*> l') (r <*> r')

instance (Arbitrary a) => Arbitrary (BinTree a) where
    arbitrary = oneof [return Empty, -- oneof :: [Gen a] -> Gen a
                liftA3 Node arbitrary arbitrary arbitrary]
                
-- Identity
apIdentityProp :: (Applicative f, Eq (f a)) => f a -> Bool
apIdentityProp v = (pure id <*> v) == v

apHomomorphismProp :: forall f a b. (Applicative f, Eq (f b)) => Fun a b -> a -> Bool
apHomomorphismProp (apply -> g) x = (pure @f g <*> pure x) == pure (g x)

main = quickCheck $ apHomomorphismProp @BinTree @Int @Int

However, when I execute the code, quickCheck applied to the applicative property returns:

(0 tests)

How can I solve this issue ?


Solution

  • Quite simply, your pure implementation generates an infinite tree. <*> preserves the infinite size of the trees on both of its sides. Then you compare the resulting infinite tree for equality with another infinite tree.

    Well, it evidently doesn't find any discrepancy between them... but it doesn't terminate either. So QuickCheck never actually manages to confirm even one test case correct.

    One way out could be to use not == but an equality operator which only checks for equality down to a limited depth, and assumes it'll be equal further down as well. (Note that it will still be exponentially expensive, so you can't even go to very great depth!)