quick check quick thoughts

actually, it's scalacheck.

用中文寫好了，英文寫不快...
以往在 unit test 中，通常是寫一段 use case,
然後比方說用 mock 確認執行順序，用 assert 確認
輸出結果。也就是說，是貨真價實的 case by case 討論。

這種作法的缺點是，你必須列舉所有可能。
而什麼應該測試，什麼不該，其實不好判斷。
有些測試太實作細節，事實上根本就不重要。
很可能稍微調整一下實作，測試就會壞掉，
然而真正的 client code, 很可能根本不受影響。

我覺得 unit test 最大的困難，就是像這樣
區分究竟哪個需要被測試，哪個不需要。比方說，
我們應該測試錯誤的行為是錯誤的，還是正確的行為
是正確的，還是不管哪一個行為都要測試？

*

讓我困惑的是，我一開始在寫 scalacheck 時，
同樣是以這種思維去寫的。於是面臨到一種問題：
我得把演算法重寫一次，或是 copypasta 過來。

這樣很蠢。同樣的演算法寫兩次，然後確保兩者一樣非常蠢。
copypasta 過來同樣蠢，這跟沒做有什麼不同？
但如果我只是要測某些輸入肯定是某些輸出，
那乾脆直接用 unit test 不就好了？？

陷入這樣的困惑中一段時間。直到這次我開始思索該如何
check 這次計算地圖周遭所有格子的演算法，才忽然意會。
事實上 quick check 要做的事，應該是迫使你去思考
演算法本身具有什麼性質？具有什麼 invariant?
類似這樣的問題才對。在這裡，我就可以檢查輸出結果的長度。

我有座標，我可以用另一種演算法算出周遭會有幾個格子。
拿這個去驗證輸出結果的長度，應該就是某種性質了。
事實上我也確實不需要這個計算長度的演算法，只是單純驗證而已。

於是我要檢查這樣的演算法是否正確，應該就是另外再寫幾個
可以描述那演算法性質的演算法。這樣就不會有重複計算的問題了。

我想，在 Agda 中就能夠把這種性質寫入 type 裡，
而不是另外再寫 quick check? 而或許能有一種機制，
是在 runtime 時能夠把這種 type 給丟棄，因此也不會有
runtime overhead. 優勢就是不需要分成兩份在寫，
程式本身就要具備有描述性質的方式。

可惜目前我駕馭不了 XD
連寫個 reverse concat 都要搞半天 @@
儘管那好像也是一兩年前的事了..? 不知道有進步多少？

==
這篇是在 20:22 才補寫完的.... 發表時間時只寫了幾行 :/
而且現在快昏倒了，不知道有沒有寫得怪怪的 XD
勉強寫東西實在不怎麼舒服... 但不寫會忘記！