1
En guise d'exercice, je suis en train de quickcheck la propriété homomorphisme de applicative:Comment vérifier rapidement la propriété d'homomorphisme applicatif?
pur f < *> pur x = pur (fx)
Lorsque je tente d'écrire la propriété dans un général manière à l'aide de types fantômes, je semble courir dans des erreurs sans fin «Impossible de déduire». À ce stade, j'ai ajouté de nombreuses annotations de type à mon code, et je reçois toujours ces erreurs.
Mon code est:
{-# LANGUAGE ViewPatterns #-}
import Test.QuickCheck (quickCheck)
import Test.QuickCheck.Function (Fun, apply)
-- | phantom type
data T a = T
-- | pure f <*> pure x = pure (f x)
prop_homomorphism :: (Applicative f, Eq b, Eq (f b)) => (T a) -> (T (f b)) -> Fun a b -> a -> Bool
prop_homomorphism T T (apply -> g) x = (pure (g :: a -> b) <*> pure x :: (Applicative f, Eq (f b)) => f b) == (pure (g x) :: (A
pplicative f, Eq (f b)) => f b)
prop_maybeint :: IO()
prop_maybeint = do
quickCheck (prop_homomorphism (T :: T Int) (T :: T (Maybe Int)))
main = do
prop_maybeint
Et les erreurs sont cela donne:
applicativehomomorphism.hs:11:40: error:
• Could not deduce (Eq (f0 b0)) arising from a use of ‘==’
from the context: (Applicative f, Eq b, Eq (f b))
bound by the type signature for:
prop_homomorphism :: (Applicative f, Eq b, Eq (f b)) =>
T a -> T (f b) -> Fun a b -> a -> Bool
at applicativehomomorphism.hs:10:1-98
The type variables ‘f0’, ‘b0’ are ambiguous
These potential instances exist:
instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Base’
instance (Eq a, Eq b) => Eq (a, b) -- Defined in ‘GHC.Classes’
instance (Eq a, Eq b, Eq c) => Eq (a, b, c)
-- Defined in ‘GHC.Classes’
...plus 13 others
...plus one instance involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the expression:
(pure (g :: a -> b) <*> pure x :: (Applicative f, Eq (f b)) => f b)
== (pure (g x) :: (Applicative f, Eq (f b)) => f b)
In an equation for ‘prop_homomorphism’:
prop_homomorphism T T (apply -> g) x
= (pure (g :: a -> b) <*> pure x ::
(Applicative f, Eq (f b)) => f b)
== (pure (g x) :: (Applicative f, Eq (f b)) => f b)
applicativehomomorphism.hs:11:41: error:
• Could not deduce (Applicative f0)
arising from an expression type signature
from the context: (Applicative f, Eq b, Eq (f b))
bound by the type signature for:
prop_homomorphism :: (Applicative f, Eq b, Eq (f b)) =>
T a -> T (f b) -> Fun a b -> a -> Bool
at applicativehomomorphism.hs:10:1-98
The type variable ‘f0’ is ambiguous
These potential instances exist:
instance Applicative IO -- Defined in ‘GHC.Base’
instance Applicative Maybe -- Defined in ‘GHC.Base’
instance Applicative ((->) a) -- Defined in ‘GHC.Base’
...plus two others
...plus two instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the first argument of ‘(==)’, namely
‘(pure (g :: a -> b) <*> pure x ::
(Applicative f, Eq (f b)) => f b)’
In the expression:
(pure (g :: a -> b) <*> pure x :: (Applicative f, Eq (f b)) => f b)
== (pure (g x) :: (Applicative f, Eq (f b)) => f b)
In an equation for ‘prop_homomorphism’:
prop_homomorphism T T (apply -> g) x
= (pure (g :: a -> b) <*> pure x ::
(Applicative f, Eq (f b)) => f b)
== (pure (g x) :: (Applicative f, Eq (f b)) => f b)
applicativehomomorphism.hs:11:47: error:
• Couldn't match type ‘b’ with ‘b2’
‘b’ is a rigid type variable bound by
the type signature for:
prop_homomorphism :: forall (f :: * -> *) b a.
(Applicative f, Eq b, Eq (f b)) =>
T a -> T (f b) -> Fun a b -> a -> Bool
at applicativehomomorphism.hs:10:22
‘b2’ is a rigid type variable bound by
an expression type signature:
forall a1 b2. a1 -> b2
at applicativehomomorphism.hs:11:52
Expected type: a1 -> b2
Actual type: a -> b
• In the first argument of ‘pure’, namely ‘(g :: a -> b)’
In the first argument of ‘(<*>)’, namely ‘pure (g :: a -> b)’
In the first argument of ‘(==)’, namely
‘(pure (g :: a -> b) <*> pure x ::
(Applicative f, Eq (f b)) => f b)’
• Relevant bindings include
g :: a -> b (bound at applicativehomomorphism.hs:11:33)
prop_homomorphism :: T a -> T (f b) -> Fun a b -> a -> Bool
(bound at applicativehomomorphism.hs:11:1)
applicativehomomorphism.hs:11:112: error:
• Couldn't match type ‘b’ with ‘b1’
‘b’ is a rigid type variable bound by
the type signature for:
prop_homomorphism :: forall (f :: * -> *) b a.
(Applicative f, Eq b, Eq (f b)) =>
T a -> T (f b) -> Fun a b -> a -> Bool
at applicativehomomorphism.hs:10:22
‘b1’ is a rigid type variable bound by
an expression type signature:
forall (f1 :: * -> *) b1. (Applicative f1, Eq (f1 b1)) => f1 b1
at applicativehomomorphism.hs:11:126
Expected type: f1 b1
Actual type: f1 b
• In the second argument of ‘(==)’, namely
‘(pure (g x) :: (Applicative f, Eq (f b)) => f b)’
In the expression:
(pure (g :: a -> b) <*> pure x :: (Applicative f, Eq (f b)) => f b)
== (pure (g x) :: (Applicative f, Eq (f b)) => f b)
In an equation for ‘prop_homomorphism’:
prop_homomorphism T T (apply -> g) x
= (pure (g :: a -> b) <*> pure x ::
(Applicative f, Eq (f b)) => f b)
== (pure (g x) :: (Applicative f, Eq (f b)) => f b)
• Relevant bindings include
g :: a -> b (bound at applicativehomomorphism.hs:11:33)
prop_homomorphism :: T a -> T (f b) -> Fun a b -> a -> Bool
(bound at applicativehomomorphism.hs:11:1)
Je me bats avec pendant un certain temps et je suis assez coincé. Quel est mon problème?
Essayez d'activer '{- # LANGUE de la # -}' et 'forall' -quantification de toutes les variables de type dans la signature que vous mentionnez dans le corps. – luqui