证明/测试的通用功能

Question

正确性（这不是定理证明是关于在实践中检验像quickCheck）

让f一些通用的功能

f :: RESTRICTIONS => GENERICS 

一些“理想”性质（即是不是黑客，是不可变的，...）通常是一个纯粹的Haskell泛型函数。

假设我们想测试一下，主要的问题是

如果我们有（井）测试该功能为某种特定类型（例如Int），我们可以假设它是正确的所有类型？（匹配的限制，当然）

（用“行之有效的”我的意思是“所有”功能{domain X properties}已经过测试）

Theorically 我们可以肯定，但是，我不知道，如果一些额外的财产，限制，...在实例化过程（即编译）可能有影响。

谢谢！

注测试也许使用某些类型的特定性质（例如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

只有在限制为空的情况下，或者至少没有提及有问题的泛型类型时，才能确定。

在所有其他情况下，您的函数取决于类实例类型的功能。但即使所有实例的行为都符合您的期望，但对于明天写入的类型实例，这不一定是正确的。

所以，这是一个在实例中强制执行某些属性的问题。这通常是一个薄弱环节，因为类型法律大多只是非正式的。例如，Haskell不能也不会阻止你制作错误的Eq或Ord实例。

一个现实世界的例子是像功能的测试：

f :: Num a => a -> a 

现在，我们知道我们有一个溢出默默地，如int类型。其他人没有。这在Num类中是默默忍受的，因为，生活就是这样。因此，一旦使用Double进行了所有测试，如果您在Int上使用f，仍然会感到惊讶。

Answer 2

不，你不能确定。

考虑

f :: (Fractional a) => a -> a 
f x = (2 * x^2 + 2)/(x^2 + 1) 

现在你会说，看样子f x ≡ 2。果然，

前奏曲>映射​​f [-2，-1.6 .. 3]
[2.0,2.0,2.0,2.0,2.0,2.0,2.0,2.0,2.0,2.0,2.0,2.0 ，2.0,2.0]

事实上，它确实适用于所有的Rational参数，以及任何非超定实数类型。然而，当你让更多的普通Fractional类型它容易破碎：

前奏Data.Complex> F（0：+ 1）
楠：+ NaN的

至关重要的一点是基本上所有 Real类型有额外的法律，特别是x^2 >= 0，这不适用于一般Num案件。

---

一个更好的例子可能是

g :: Num a => a -> a 
g = (+1) 

直观，g x > x，它适用于所有Integer秒。但是，这其实不一定是真实的......

前奏Data.Modular>地图（（（X ::ℤ/ 5） - > GX> X）fromInteger。）[0 .. 10]
[真，真，真，真，假，真，真，真，真，假，真]

---

Disconsidering如与数值问题Double。