推 SansWord:Cool! Thanks! 06/04 00:58
因為有人提到，所以複習了一下..
1. Y combinator in Haskell
Y combinator 在 untyped lambda calculus 中是
\f -> (\x -> f (x x)) (\x -> f (x x))
試著寫成 Haskell:
y :: (a -> a) -> a
y f = (\x -> f (x x)) (\x -> f (x x))
f 的型別是 a -> a, 而 y 取 f 的 fixed-point，
所以 y 的型別是 (a -> a) -> a.
但是這個型別一看就有問題：把 type 看成邏輯的話，
這個 type 若有證明就會有 inconsistency. 果然， Haskell
不讓這個程式 typecheck:
Occurs check: cannot construct the infinite type: t = t -> a
Probable cause: `x' is applied to too many arguments
In the first argument of `f', namely `(x x)'
In the expression: f (x x)
操作上的理由是：在 (x x) 之中，x 的型別又是 t -> a, 又是 t, 而
t = t -> a 遞迴定義。
解決方法也很簡單，就頭痛醫頭腳痛醫腳，做一個 t 與 t -> a
同構的遞迴型別囉。
data Fix a = Rec (Fix a -> a) -- Fix a 和 Fix a -> a 同構
有了 Fix 就可以寫 Y combinator 了。
y :: (a -> a) -> a
y f = (\(Rec x) -> f (x (Rec x)))
(Rec (\(Rec x) -> f (x (Rec x))))
和前一個版本比較，這裡多了很多 Rec，其實是在告訴 typechecker
何時要把 Fix 展開。
2. 用 Y 定義遞迴函數
假設 Haskell 不允許遞迴定義（正確地說，允許遞迴資料型別，但
不允許遞迴的 term），那要怎麼寫遞迴函數呢？
遞迴版本的階層是這麼寫的:
fact :: Int -> Int
fact 0 = 1
fact (n+1) = (n+1) * fact n
沒有遞迴的話，就用 Y 取 fixed-point 囉。首先定義這個 factF:
factF :: (Int -> Int) -> (Int -> Int)
factF g 0 = 1
factF g (n+1) = (n+1) * g n
和 fact 的差別是 factF 只做 fact 的第一層。注意 factF 的型別。
然後 fact 就是 factF 的 fixed-point:
fact :: Int -> Int
fact = y factF
由此可知一個語言如果有提供 closure, 就可以不用把遞迴當作
primitive.
3. Mutual Recursion
Mutual recursion 其實也是一樣的，只是同時定義一組東西。
比如說一般 even 和 odd 可以這樣定:
even, odd :: Int -> Bool
even 0 = True
even (n+1) = odd n
odd 0 = False
odd (n+1) = even n
如果沒有遞迴，就定義一個從「一對」函數到一對函數的函數:
evenOddF :: (Int -> Bool, Int -> Bool) -> (Int -> Bool, Int -> Bool)
evenOddF (ev, od) =
(\n -> if n == 0 then True else od (n-1),
\n -> if n == 0 then False else ev (n-1))
evenOddF 拿一對函數 (ev,od)，產生一對函數，各自只做 even 和 odd
的第一層。本來該是遞迴的地方分別呼叫 od 和 ev.
（如果該語言沒有 pair, 就用 lambda 來模擬。）
然後我們也用 Y 取 evenOddF 的 fixed-point:
evenOdd :: (Int -> Bool, Int -> Bool)
evenOdd = y evenOddF
even 就是第一個，odd 就是第二個:
even = fst evenOdd
odd = snd evenOdd
只是還有一點小問題：在 Haskell 中 y evenOddF 不會終止。
簡單的解決方法是把
evenOddF (ev, od) = ... od .. ev ...
改成
evenOddF evod = ... snd evod ... fst evod ...
看起來比較漂亮，其實一樣的方法是用 lazy pattern:
evenOddF ~(ev, od) = ... od .. ev ...
這樣就可以囉！
*Main> even 10
True
*Main> odd 10
False
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 123.192.160.134