generics - 证明/测试泛型函数的正确性

Question

(这不是关于定理证明，而是关于实践中的测试，例如 quickCheck)

让f一些通用函数

f :: RESTRICTIONS => GENERICS

具有一些“理想的”属性(即不是 hack，是不可变的，...)，通常是纯 Haskell 泛型函数。

假设我们要测试它，主要问题是

如果我们(很好)测试了该函数针对一种特定类型(例如 Int)，我们可以假设它对于所有类型都是正确的吗？(匹配限制，当然)

(“经过充分测试”是指“所有”函数{domain X properties}都已测试)

理论上我们可以确定，但是，我不确定实例化过程(即编译)中的一些附加属性、限制等是否可能产生影响。

谢谢!

注意测试可能会使用某些类型特定的属性(例如Int)，但这些属性不能成为测试属性的一部分。例如。如果Monoid是一个限制，那么关联性可以成为测试属性的一部分(但如果不是限制则不是交换性)。

示例

让f

repeatedHeader :: Eq a => [a] -> Bool
repeatedHeader (x:y:_) = x == y
repeatedHeader _ = False

test1 = repeatedHeader [1,1,2] == True
test2 = repeatedHeader [1,2,3] == False

Answer 1

只有在微不足道的情况下，您才能确定 RESTRICTIONS 为空，或者至少没有提及相关的泛型类型。

在所有其他情况下，您的函数取决于类型类实例的功能。但是，即使所有现有实例的行为都符合您的预期，对于明天编写的类型类实例也不一定如此。

因此，这是一个在实例中强制执行某些属性的问题。这通常是一个弱点，因为类型类法大多只是非正式地表述。例如，Haskell 不能也不会阻止您创建错误的 Eq 或 Ord 实例。

现实世界的示例是对如下函数的测试:

f :: Num a => a -> a

现在，我们知道确实有静默溢出的类型，例如 Int。其他人则不然。这在 Num 类中是默默容忍的，因为，生活就是这样。因此，一旦您使用 Double 完成了所有测试，如果您在 Int 上使用 f，您仍然会感到惊讶。