haskell - 快速检查有关长度索引列表的属性

Question

我正在尝试使用 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 .

Answer 1

这里有两个相同问题的实例。第一个实例是导致错误消息的实例。第二个实例只有在你解决了第一个问题后才会出现，而且会更难解决。

当您的类型过于笼统时，错误消息来自一个常见问题。相同错误的一个更简单的示例是函数:

-- 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)