What have you found for these years?

2011-05-17

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 list0,
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 好啊 (誤)


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

0 retries:

Post a Comment

All texts are licensed under CC Attribution 3.0