pattern matching, strict or non-strict?

為了整理這篇，才注意到在 denotational programming 那篇所提到的
newtype/data pattern matching strictness 的部份應該是錯的。

急忙補了這段更新，希望還來得及...

updated: 2011-05-08 13:14 後來自己實驗發現 data/newtype
其實沒有 strictness 上的差別，Learn You a Haskell for Great Good!
這邊有點誤導...

既然如此，這邊就拿書中的例子來說好了。在第 12 章的 Monoids,
On newtype Laziness, p247. 裡面有這個 data 定義：

data CoolBool = CoolBool { getCoolBool :: Bool }

用在這個 function 中：

helloMe :: CoolBool -> String
helloMe (CoolBool _) = "hello"

如果在 ghci 中跑 helloMe undefined 則會產生 exception, 而不是
在 non-strict 情況下的 "hello". 反之，如果 CoolBool 是用 newtype 定義：

newtype CoolBool = CoolBool { getCoolBool :: Bool }

則可以正確得到 "hello". 因此我錯把這理解成 newtype 跟 data 的
pattern matching 不一樣。而事實上，雖然在這測試中，helloMe 的
定義並沒有改變，但兩者語意是不一樣的...

newtype 那邊不應理解成 pattern matching. 原因其實也跟書上說的一樣，
newtype 的 constructor 真相永遠只有一個，因此也可以說是只有唯一
一個可能的 match. 照原本 helloMe 的定義，那邊的意思比較接近：

helloMe :: CoolBool -> String
helloMe cool_bool = let bool = getCoolBool cool_bool
                    in "hello"

這樣應該可以很容易看出其實沒有任何 pattern matching, 不管是
newtype 或 data 都因此不會有任何 exception. 而如果真的寫
helloMe (CoolBool True) 的話，則兩者都會有 exception,
因為兩者都要去看 undefined 到底是不是 True.

到這裡，不禁就要想，data CoolBool 也是只有唯一的 constructor,
何不也使得他運作得像是 newtype? 不過我猜這樣會使得 programmer
更困惑吧。像是原本只有一個 constructor, 後來改成兩個，結果導致語意
改變？

* * *

因此，newtype 應視為一種 wrapper, 上面寫 CoolBool _ 應視為用
getCoolBool 的 function call, 而非 pattern matching. 講到 pattern
matching, 看到現在似乎全部都是 strict 的...

但再回頭看看
Unraveling the mystery of the IO monad
裡面提到了 irrefutable pattern.... 我之前從來沒聽過 :s

看起來他的意思是，聲稱這個 pattern 一定必須 match, 因此程式一定是
選擇這個 function, 而非其他 partial function. 也因為已經決定了要選擇
哪個 function, 使得這個 pattern matching 可以是 non-strict 的。

另一方面，昨天還看到一封在 Haskell-cafe 回應 Monad law 的信。
裡面提到 seq undefined 42 會有 exception, 但
seq (id . undefined) 42 卻不會。作者說：

So (id . undefined) /= undefined, violating one of the category laws.
This is not just a problem with IO - it's a problem with Haskell itself.

要解決這個問題，可以定義 strict composition...

(.!) :: (b -> c) -> (a -> b) -> a -> c
f .! g = f `seq` g `seq` f . g

這樣 seq (id .! undefined) 42 就會有 exception 了。解釋：

This is "true" function composition in the mathematical
sense - it doesn't have the extra layer of laziness that
Haskell usually imposes. With strict composition,
Haskell types and functions do form a category even
when we include seq.

Unfortunately, IO still does not satisfy the monad laws.
But that could easily be fixed by making return strict,
so that return undefined == undefined. (Note also that
by "monad laws" here I mean the points-free version of the
laws, with strict composition. That is the version of the
laws we get if take the mathematical monad laws
in the category we have just defined and translate them
into Haskell monad notation.)

最後，附上測試用的一些例子。本來想直接 embed gist, 不過發現
gist 背景是亮的，放在我這看起來太刺眼了點。strictness.hs
以下只列出兩個跟 irrefutable pattern 有關的：

-- always True
-- Warning: Pattern match(es) are overlapped
test7 :: Bool -> Bool
test7 ~True = True
test7 False = False

-- undefined -> exception undefined
-- True      -> True
-- False     -> exception irrefutable pattern failed
-- Warning: Pattern match(es) are overlapped
test8 :: Bool -> Bool
test8 ~true@True = true
test8 False = False

---

這幾天寫太多 haskell 的東西了，好累 orz 覺得需要一個人幫忙編輯....
自己在那邊琢磨字句真的很傷腦筋 :s

不過最累的應該是因為邊寫邊發現前面寫好的被推翻了 :o
這表示不要在還沒搞清楚狀況之前就寫下來 XD
但不寫不整理的話，又不會特別去找資料來試著佐證，
然後才發現其實自己的理解錯了..... Orz