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 ?
CodePudding user response:
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!)