How to check this applicative example using checkers? (There is no instance for CoArbitrary (check e0 [Char]))

Checkers is a library for multiple QuickCheck properties, especially for standard type classes

How to write a checkers instance to check if my applicative Validation instance is valid?

import Test.QuickCheck import Test.QuickCheck.Checkers import Test.QuickCheck.Classes import Control.Applicative import Data.Monoid data Validation ea = Error e | Scss a deriving (Eq, Show) instance Functor (Validation e) where fmap _ (Error e) = Error e fmap f (Scss a) = Scss $ fa instance Monoid e => Applicative (Validation e) where pure = Scss (<*>) (Scss f) (Scss a) = Scss $ fa (<*>) (Error g) (Scss a) = Error g (<*>) (Scss a) (Error g) = Error g (<*>) (Error a) (Error g) = Error $ mappend ag instance (Arbitrary a, Arbitrary b) => Arbitrary (Validation ab) where arbitrary = do a <- arbitrary b <- arbitrary elements [Scss a, Error b] instance (Eq a, Eq b) => EqProp (Validation ab) where (=-=) = eq main :: IO () main = quickBatch $ applicative [(Scss "b", Scss "a", Scss "c")] 

I think I'm almost there, but I get an error:

 chap17/Validation_applicative.hs:36:21: No instance for (CoArbitrary (Validation e0 [Char])) … arising from a use of 'applicative' In the second argument of '($)', namely 'applicative [(Scss "b", Scss "a", Scss "c")]' In the expression: quickBatch $ applicative [(Scss "b", Scss "a", Scss "c")] In an equation for 'main': main = quickBatch $ applicative [(Scss "b", Scss "a", Scss "c")] Compilation failed. 

I tried to add a CoArbitrary instance for validation as follows:

 instance CoArbitrary (Validation ab) 

but this leads to this error message:

 chap17/Validation_applicative.hs:35:10: No instance for (GHC.Generics.Generic (Validation ab)) … arising from a use of 'Test.QuickCheck.Arbitrary.$gdmcoarbitrary' In the expression: Test.QuickCheck.Arbitrary.$gdmcoarbitrary In an equation for 'coarbitrary': coarbitrary = Test.QuickCheck.Arbitrary.$gdmcoarbitrary In the instance declaration for 'CoArbitrary (Validation ab)' chap17/Validation_applicative.hs:38:21: No instance for (Eq e0) arising from a use of 'applicative' … The type variable 'e0' is ambiguous Note: there are several potential instances: instance Eq a => Eq (Const ab) -- Defined in 'Control.Applicative' instance Eq a => Eq (ZipList a) -- Defined in 'Control.Applicative' instance Eq a => Eq (Data.Complex.Complex a) -- Defined in 'Data.Complex' ...plus 65 others In the second argument of '($)', namely 'applicative [(Scss "b", Scss "a", Scss "c")]' In the expression: quickBatch $ applicative [(Scss "b", Scss "a", Scss "c")] In an equation for 'main': main = quickBatch $ applicative [(Scss "b", Scss "a", Scss "c")] Compilation failed. 
+3
source share
1 answer

how

To automatically get a CoArbitrary instance, your data type must have a Generic instance, which again can be automatically retrieved using some nice language extension:

 {-# LANGUAGE DeriveGeneric #-} import GHC.Generics data Validation ea = Error e | Scss a deriving (Eq, Show, Generic) 

However, the most significant mistake in your program is that you tested [] , but not your own applicative [(Scss "b", Scss "a", Scss "c")] type applicative [(Scss "b", Scss "a", Scss "c")] . here is the definition of the applicative test package, details are omitted:

 applicative :: forall mab c. ( Applicative m , Arbitrary a, CoArbitrary a, Arbitrary b, Arbitrary (ma) , Arbitrary (m (b -> c)), Show (m (b -> c)) , Arbitrary (m (a -> b)), Show (m (a -> b)) , Show a, Show (ma) , EqProp (ma), EqProp (mb), EqProp (mc) ) => m (a,b,c) -> TestBatch applicative = const ( "applicative" , [ ("identity" , property identityP) , ("composition" , property compositionP) , ("homomorphism", property homomorphismP) , ("interchange" , property interchangeP) , ("functor" , property functorP) ] ) 

In short, for the four types m , a , b and c this function will create a bunch of properties that m - as an application functor - must satisfy, and then you can check them with random a b c values ​​generated by QuickCheck . [(Scss "b", Scss "a", Scss "c")] has the type [(Validation String, Validation String, Validation String)] does m ~ [] .

So, you should specify some value of type Validation e (a, b, c) or not at all: you may have noticed const in the definition of applicative , only the type of the argument matters:

 main :: IO () main = quickBatch $ applicative (undefined :: Validation String (Int, Double, Char)) 

After that, you can run the test and get a well-formatted result. But no, you should not take the applicative approach this way.


Why should not

The test provided by checkers is far from sufficient. In terms of the GHC monomorphism execution time and how it relates to ambiguity, you must provide four specific, non-polymorphic types for testing, for example, Validation String (Int, Double, Char) , and the test module will only generate and test those four types in while your application functor should work with any type appropriate to the context.

IMO, most polymorphic functions do not fit well into the unit test structure: it cannot be tested on all possible types, so you need to either conduct some kind of test in any case with manually selected types, or run a type test that is fairly general (for example, Free monad, when your code requires an arbitrary monad, but usually "fairly general" is not defined in other contexts).

It is better to strictly study your implementation and prove all the laws that satisfy all cases, whether it be a pen and paper or some kind of proof engine, such as agda. Here is an example on Maybe that may help: Proof of the composition law, possibly of the applicant


EDIT: read the comment. I don’t quite understand this, but it means that Integer is a “common enough” type for unit testing polymorphic functions. I found this article on Bartosh Milevsky’s blog and its bibliography of good resources for mastering the idea of ​​parametricity and a free theorem.

+8
source

Source: https://habr.com/ru/post/1273511/


All Articles