3

（这不是关于定理证明，而是关于实践中的测试，例如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
4

2 回答 2

2

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

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

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

一个现实世界的例子是对一个函数的测试，比如：

f :: Num a => a -> a

现在，我们知道我们确实有无声溢出的类型，比如 Int。其他人没有。这在 Num 类中是默默容忍的，因为，好吧，生活就是这样。因此，一旦你使用了所有测试，Double如果你使用fon ，你仍然会感到惊讶Int。

于 2013-11-28T09:33:22.913 回答
1

不，你不能确定。

考虑

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

你现在会说，显然f x ≡ 2。果然，

前奏> map 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类型时，它很容易被破坏：

Prelude Data.Complex> f (0 :+ 1)
NaN :+ NaN

关键点基本上是所有1 Real类型都有额外的法律，特别是x^2 >= 0，这不适用于一般Num情况。

一个更好的例子可能是

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

直观地说，g x > x它适用于所有Integers。但这实际上并不一定是真的……

Prelude Data.Modular> map (((x :: ℤ/5) -> gx > x) . fromInteger) [0 .. 10]
[True,True,True,True,False,True,True,True,True,假，真]

1考虑数字问题，例如Double。

于 2013-11-28T08:45:32.303 回答