Home > Software design >  Quickcheck Applicative homomorphism law for Binary Tree
Quickcheck Applicative homomorphism law for Binary Tree

Time:01-19

I am aware that the following question exists:

haskell - How to quickcheck applicative homomorphism property? - Stack Overflow

However, the introduction of the following PRAGMA

{-# LANGUAGE ScopedTypeVariables #-}

didn't solve my issue.

These are my definitions:

{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Laws where

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

import Data.Monoid

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

newtype BinTree a = Empty | Node a (ArbolBin a) (ArbolBin 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 ArbolBin 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

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

main :: IO ()
main = quickCheck (apHomomorphismProp :: Fun Int Int -> Int -> Bool)

How can I fix the following error ?

Could not deduce (Applicative f0) from the context: (Applicative f, Eq (f b))

CodePudding user response:

It would have been easier to analyse the problem if you had included the full error message, which mentions an ambiguous type variable. The thing that GHC is complaining about is that f does not appear anywhere in the type signature of apHomomorphismProp, except in the quantifier and constraints.

Why is that a problem? Well, it isn't a problem... but it used to be in older Haskell versions, because there was no way for the compiler to tell when you're using apHomomorphismProp what applicative it's supposed to test here. In fact this is still the case with the way you are using it: apHomomorphismProp :: Fun Int Int -> Int -> Bool does not mention BinTree in any way, so how is the compiler supposed to know that's what you mean? For all it knows, you could as well be asking for, say, the Maybe applicative to be tested here.

The solution, in modern Haskell, is -XTypeApplications, which just lets you explicitly say what a type variable should be instantiated with.

{-# LANGUAGE TypeApplications #-}

main = quickCheck (apHomomorphismProp @BinTree :: Fun Int Int -> Int -> Bool)

In fact I would recommend also using this syntax to clarify the Int types:

main = quickCheck $ apHomomorphismProp @BinTree @Int @Int

However, there was still the compiler error with apHomomorphismProp, which is all because prior to TypeApplications, a signature like the one you gave to apHomomorphismProp was useless. But this restriction is now obsolete, and it can be disabled with -XAllowAmbiguousTypes:

{-# LANGUAGE ScopedTypeVariables, UnicodeSyntax, AllowAmbiguousTypes, TypeApplications #-}

apHomomorphismProp :: ∀ 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)

Note that I only need to mention @f for one of the pures, the other ones are automatically constrained to the same applicative.


It's arguable whether it's really obsolete. What's probably still true is that if a beginner gives their function an ambiguous type, it's more likely a mistake that should be caught right there and then, rather than something that's actually intended for use with -XTypeApplications. An unintentionally ambiguous type can cause quite confusing errors further down the line.

  • Related