證明/測試的通用功能

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。