strictness, laziness, and termination

自從讀了 The Point of Laziness 之後，想了很多這方面的問題......

一個不是很容易區分的概念是，non-strict 跟 lazy evaluation (call by need)
要如何區別？就我最早的理解，前者是概念，後者是實作，也就是說，可能有其他
方式來達到 non-strict.

後來的理解則是，strictness 表達的是 const unit ⊥ 究竟會是 unit 還是 ⊥,
跟 evaluation 倒沒有直接的關係。只要 const unit ⊥ 可以是 unit, 則算是
non-strict, 反之則是 strict.

不過要明確地區分，或許還是找到另一種實作 non-strict 的方式，會比較
容易理解。後來想了很多 pattern matching 和 strictness 之間的關係後，
大概得到一些結論。

想像一個 haskell 程式就是一個巨大的 term, 而所謂 execute, 或所謂的
evaluation, 其實就是把整個巨大的 term, reduce 成最小的 normal form.

這在 eager (call by value) 程式裡，應該是沒什麼問題，反正就是全部都
reduce 掉就對了。strict 程式應該亦然，反正只要某個地方得到 ⊥, 整個程式
就是 ⊥ 了。這裡先不考慮可以被 catch (rescue) 的 exception.... 先假設
一旦發生 exception, 整個程式就是 ⊥. 程式不會 terminate, 反正也是 ⊥,
差別在前者我們知道程式 crash 了，後者則面臨 halting problem.

lazy evaluation (call by need) 則讓人玩味了。究竟什麼時候，或是說哪個
地方，才應該是「引爆點」？哪個地方是那個 "need" ? 以 haskell 而言，
大概就是 main 這個 IO monad (action) 吧。但引爆之後，究竟是誰要爆？

我覺得我一直卡在這個問題上。雖然這樣講或許有點倒果為因，但感覺上
只要是被 main 用 IO monad 的 bind 給 bound 住的 IO monad, 就會被
evaluate, 然後順著一路 evaluate 到 (some kind of) normal form.

但除了 IO monad 的 bind 外，我們要怎麼求得一個 pure value?
似乎還是需要某種「強迫」，或是說某種方式表達我們真的 "need" 那個 value.
假使 pattern matching 是 strict, 則這一切都很好處理。因為我們就可以靠
pattern matching 來「強迫」取得某個 value, 於是程式就能順利執行下去...

另一方面，我們知道 lazy evaluation 其實是在身上掛無數的包裹，或說肉團...
上面所提到的「強迫」，就是打開這個包裹，或是割掉這塊肉的動作。算了，
我還是不要形容成肉塊好了，有點怪。總而言之，會有非常多懸而未決的包裹，
我們不知道究竟什麼時候要打開那些包裹，也不知道包裹裡面究竟還有多少
包裹。如果 pattern matching 是 lazy 的，意味著包裹裡面也會有很多的
"branch", 也就是非常有可能是一個很巨大的 term (包裹). 如果有太多
懸而未決的這些東西，現實上，很可能會吃掉太多的記憶體。

我想這也是為什麼聽說很多 haskell 程式，會有很恐怖的記憶體用量歷史圖。
裡面很可能就是懸著一個太過於巨大的包裹。懸著太大的包裹，吃掉太多記憶體
(space), 面臨打開的時候，很可能又變成瞬間面臨太多的運算 (time).

這或許是 lazy evaluation 的一個問題，但似乎不是 non-strict 的問題。

假使我們有某種方法，可以把整個 program 的這個 term, 一切為四個 sub-term,
然後分別交由四個 core 去 eagerly (non-lazy) 運算，同時由於我們希望程式
本身是 non-strict 的，因此碰上 ⊥ 時，就應該忽略他，除非我們現在真的 "need" 的
那個 value 也 "need" 這個 ⊥, 不然 const unit ⊥ 還是應該 reduce 成 unit.

可惜理論上這是不可能的，因為這面臨了 halting problem. 我們可以知道
exception 的 ⊥, 但沒辦法知道 non-terminating 的 ⊥, 因此希望透過事先運算
來避免攜帶太大的包袱，又能同時達到 non-strict 的性質，或許是無解的。
折衷方式或許是，給定一定的運算時間，如果超過了，則跳開先算其他的 sub-term....
也就是說，語意上或許仍然是 lazy evaluation, 實際上卻偷偷在別人背後拆禮物，
如果發現某個禮物一時拆不完，就跳過先拆其他的小禮物..... 雖然可能浪費了時間
拆開了用不到的禮物（裡面是磚塊），但至少或許可以減緩攜帶太大包的問題。

說來好像很簡單，實際上這運作起來應該會異常複雜恐怖吧...
似乎是某種極端複雜的 scheduling 問題？

但如果達成了，或許可以看成是某種 non-strict 程式，但不是 lazy 的？

另外，要做這種分析，確實就需要區分各種不同的 ⊥, 這樣我們才會知道
某個 term 到底是不是真的 ⊥, 因為只要他沒有 "need" 到那個 ⊥, 他就可以
不是 ⊥.

假使我們有個 list = [0, ⊥1, 2, ⊥3], 那麼 head list 是 0,
head (tail list) 是 ⊥list-1, 依此類推，也意味著我不能把
他們全部 reduce 成一個東西，還是得把這些東西都當成一個不能
reduce 的 term (包裹) 看待...

那豈不是還是沒解決包裹太大的問題？

於是就能理解為什麼 non-strict 的程式很討厭，一大堆 ⊥ 很討厭了...

可話說回來，ruby 很好用，沒人理解 ruby 程式是怎麼運作的，
以「寫程式」的觀點來看，其實我也不想搞清楚那些 ⊥ 是怎麼回事。
反正我開心就只試著「描述」程式，我不管我描述出來的程式，是不是
其實有 20% 是一坨完全用不到的贅肉，是完全不合理的大便程式，
我只管我實際上真正跑出來的對不對就好了。

其實寫 ruby 是抱持著這種心情在寫的。所以很愉快，像在隨意塗鴨，
毫無理由地任意描繪揮灑。

那麼，可不可以也這樣說，用 haskell 寫著摻雜各種 ⊥ 的程式，
各種不合理的程式，其實也無所謂？更何況 haskell 寫出來的程式，
本來就遠比 ruby 要來得合理多了？

反正 haskell 又不是 theorem prover?

另一方面，單就只是 strict 的程式，面臨 ⊥ 一樣還是無解（吧？）
那是否乾脆就像 agda 那樣，做最嚴格的 termination check,
需要給 type checker 各種 proofs, 告訴他我的程式一定會
terminate? 這不是比 strict 程式要來得更加「正確」嗎？

所以還是 haskell 和 ruby 好啊 (誤)

---

可惡，都沒有時間好好想好好寫 ><