1
、私はquickCheckに応用的の準同型プロパティしようとしています：私は一般的なプロパティを記述しようとすると適用可能な準同形性を迅速にチェックするには？練習として
< F純粋*>純粋X =（FX）純粋
をファントムの種類を使用して、私は無限のエラーを推論できないように見える。この時点で、私はコードに多くの型の注釈を追加しましたが、まだこれらのエラーが発生しています。
{-# 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
そして、これが与えるエラーは以下のとおりです：
私のコードがある
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)
私はしばらくの間、これと戦うとかなりこだわっていてきました。私の問題は何ですか？
'を有効にしてください、その後'と 'forall' - あなたが本文で言及している署名の型変数をすべて確認します。 – luqui