我正在尝试使用 QuickCheck 来测试 Haskell 中有关长度索引列表(也称为向量)的属性。我的问题是 GHC 提示在 main
函数的 Show
约束上出现了一个不明确的变量。
我已经用标准方式定义了向量
data Nat = Z | S Nat
data Vec :: Nat -> * -> * where
Nil :: Vec 'Z a
(:>) :: a -> Vec n a -> Vec ('S n) a
vlength :: Vec n a -> Int
vlength Nil = 0
vlength (_ :> xs) = 1 + vlength xs
我已经定义了一个将它转换为列表的函数
toList :: Vec n a -> [a]
toList Nil = []
toList (x :> xs) = x : (toList xs)
这样的转换函数应该保留长度,它有一个立即编码作为一个属性:
toList_correct :: Show a => Vec n a -> Bool
toList_correct v = vlength v == length (toList v)
我已经为 Vec
定义了 Arbitrary
实例:
instance (Show a, Arbitrary a) => Arbitrary (Vec 'Z a) where
arbitrary = return Nil
instance (Show a, Arbitrary a, Arbitrary (Vec n a)) => Arbitrary (Vec ('S n) a) where
arbitrary
= (:>) <$> arbitrary <*> arbitrary
当我在 main
上调用 quickCheck 函数时出现问题:
main :: IO ()
main = quickCheck toList_correct
GHC 给我以下信息:
Ambiguous type variable ‘a0’ arising from a use of ‘quickCheck’
prevents the constraint ‘(Show a0)’ from being solved.
Probable fix: use a type annotation to specify what ‘a0’ should be.
These potential instances exist:
instance [safe] Show Args -- Defined in ‘Test.QuickCheck.Test’
instance [safe] Show Result -- Defined in ‘Test.QuickCheck.Test’
instance (Show a, Show b) => Show (Either a b)
-- Defined in ‘Data.Either’
...plus 27 others
...plus 65 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the expression: quickCheck toList_correct
In an equation for ‘main’: main = quickCheck toList_correct
我不知道如何解决这个错误。任何提示都非常受欢迎。
完整代码可用here .
最佳答案
这里有两个相同问题的实例。第一个实例是导致错误消息的实例。第二个实例只有在你解决了第一个问题后才会出现,而且会更难解决。
当您的类型过于笼统时,错误消息来自一个常见问题。相同错误的一个更简单的示例是函数:
-- Ambiguous type variable ‘a0’ arising from a use of ‘read’
showRead :: String -> String
showRead = show . read
简而言之,GHC 知道您将创建某种类型 a
的中间值(使用 read::Read a => String -> a
)然后您立即将其转换回 String
(使用 show::Show a => a -> String
)。问题是要运行它,GHC 确实需要知道您正在阅读和展示的内容的类型 - 但它无法弄清楚这一点。
类型变量a
不明确
GHC 告诉您,当它使用 toList_correct
时,它无法告诉您希望 quickCheck
测试哪种类型的向量。一种解决方法是添加类型注释(或使用 TypeApplications
)并告诉 GHC 您想要什么类型的向量:
quickCheck (toList_correct :: Vec n () -> Bool)
类型变量n
不明确
但是,不仅a
是有歧义的,n
也是!因为您正在将其长度编码到向量的类型中,所以您将只能快速检查特定长度向量的属性。简单的解决方法是确定一个特定的长度(或几个长度)。
quickCheck (toList_correct :: Vec Z () -> Bool)
quickCheck (toList_correct :: Vec (S Z) () -> Bool)
quickCheck (toList_correct :: Vec (S (S Z)) () -> Bool)
也就是说,这感觉(而且应该如此)有点毫无意义 - 您想要测试任意长度的向量。解决这个问题的方法是在你的向量周围创建一个存在类型 BoxVector
:
data BoxVector a where
box :: Vec n a -> BoxVector a
deriving instance Show a => Show (BoxVector a)
现在我们有了这个存在类型,我们可以创建它的一个 Arbitrary
实例,它甚至在向量的长度上都是任意的:
instance (Show a, Arbitrary a) => Arbitrary (BoxVector a) where
arbitrary = fromList <$> arbitrary
where
fromList :: [a] -> BoxVector a
fromList = foldr (\e (Box es) -> Box (e :> es)) (Box Nil)
我们可以在 GHCi 上将这个任意实例与您之前的实例(我们不需要)进行比较:
ghci> sample (arbitrary :: Gen (Vec (S (S Z)) Int)) -- must specify length
(:>) 0 ((:>) 0 Nil)
(:>) 1 ((:>) 1 Nil)
(:>) 0 ((:>) (-2) Nil)
(:>) (-4) ((:>) (-6) Nil)
(:>) (-1) ((:>) 2 Nil)
(:>) (-8) ((:>) (-5) Nil)
(:>) (-11) ((:>) 4 Nil)
(:>) (-8) ((:>) 2 Nil)
(:>) (-8) ((:>) (-16) Nil)
(:>) (-16) ((:>) (-11) Nil)
(:>) 19 ((:>) (-6) Nil)
ghci> sample (arbitrary :: Gen (BoxVector Int)) -- all lengths generated
Box Nil
Box ((:>) (-2) ((:>) 0 Nil))
Box ((:>) (-4) Nil)
Box ((:>) 0 ((:>) (-2) ((:>) (-6) ((:>) (-3) ((:>) (-6) Nil)))))
Box ((:>) 8 Nil)
Box ((:>) 6 ((:>) (-6) ((:>) 9 Nil)))
Box ((:>) 5 ((:>) 4 ((:>) 4 ((:>) (-6) ((:>) (-6) ((:>) (-4) Nil))))))
Box ((:>) (-4) ((:>) 10 ((:>) (-10) ((:>) 2 ((:>) 6 ((:>) 3 ((:>) 4 ((:>) 1 ((:>) 3 Nil)))))))))
Box ((:>) 10 ((:>) (-16) ((:>) (-14) ((:>) 15 ((:>) 4 ((:>) (-7) ((:>) (-5) ((:>) 5 ((:>) 6 ((:>) (-1) ((:>) 1 ((:>) (-14) ((:>) (-4) ((:>) 15 Nil))))))))))))))
Box ((:>) (-2) ((:>) 9 ((:>) 0 ((:>) 7 ((:>) 5 ((:>) 17 Nil))))))
Box ((:>) (-19) ((:>) (-7) ((:>) (-17) ((:>) (-8) ((:>) (-16) ((:>) 16 ((:>) (-4) ((:>) 16 ((:>) 13 ((:>) (-7) ((:>) (-3) ((:>) 4 ((:>) (-6) ((:>) (-8) ((:>) (-14) Nil)))))))))))))))
现在,我们终于可以让您进行测试了。由于我们希望测试运行所有可能的长度,因此我们需要将其更改为采用 BoxVector
而不是 Vec
。
toList_correct :: Show a => BoxVector a -> Bool
toList_correct (Box v) = vlength v == length (toList v)
最后,我们仍然需要指定我们的向量将包含哪些内容用于测试。对于这个测试,由于我们不关心将向量的元素彼此区分,不妨将它们设为 ()
的向量。
main :: IO ()
main = quickCheck (toList_correct :: BoxVector () -> Bool)
关于haskell - 快速检查有关长度索引列表的属性,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/39755675/