Haskell/Fix 和遞迴
乍一看，fix 函式可能顯得奇怪且無用。然而，它的存在有理論上的原因：將其作為原語引入 (型別化) lambda 演算 使你能夠定義遞迴 函式。
fix 的定義很簡單：
fix :: (a -> a) -> a
fix f = let {x = f x} in x
這看起來是不是很...神奇？你可能想知道：fix f 難道不會導致 f 無限巢狀應用的無限序列嗎？比如：x = f x = f (f x) = f (f (f ( ... )))？這裡問題的解決方案是惰性求值。本質上，如果（且僅當）f 是一個惰性函式，那麼這個無限的 f 應用序列將被避免。讓我們看一些例子。
例子： fix 的例子
Prelude> :m Control.Monad.Fix Prelude Control.Monad.Fix> fix (2+) -- Example 1 *** Exception: stack overflow Prelude Control.Monad.Fix> fix (const "hello") -- Example 2 "hello" Prelude Control.Monad.Fix> fix (1:) -- Example 3 [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,...
我們首先匯入 Control.Monad.Fix 模組，將 fix （也被 Data.Function 模組匯出）引入作用域。然後，我們嘗試三個例子。讓我們試著看看第一個例子中實際發生了什麼。
-- fix f = let {x = f x} in x
fix (2+)
= let {x = 2 + x} in x
= let {x = 2 + x} in 2 + x
= let {x = 2 + x} in 2 + (2 + x)
= let {x = 2 + x} in 2 + (2 + (2 + x))
= let {x = 2 + x} in 2 + (2 + (2 + (2 + x)))
= ...
第一個例子使用 (+)，這是一個 急切 函式；它需要知道 x 的值才能計算...x 的值。因此，這個計算永遠不會停止。現在讓我們看看第二個例子。
fix (const "hello")
= let {x = const "hello" x} in x
= let {x = const "hello" x} in const "hello" x
= let {x = const "hello" x} in "hello"
= "hello"
這非常不同：我們注意到，在 fix 展開一次之後，求值很快就會終止，因為 const 忽略了它的第二個引數。最後一個例子的求值有點不同，但我們可以用類似的方法進行。
fix (1:)
= let {x = 1 : x} in x
= let {x = 1 : x} in 1 : x
這裡 1 : x 已經處於 弱首正規化 中（(:) 是一個惰性資料建構函式），因此展開停止。這實際上建立了一個迴圈結構。每次消費者函式請求此列表的新元素時，都會查詢 x 的定義，並且它已經被知道是 1 : x。
因此，按順序請求此列表中的元素將不斷返回 1，沒有限制。所以 take 10 (fix (1:)) 將產生一個包含十個 1 的列表，但是嘗試透過在 GHCi 中鍵入 fix (1:) 來列印它們，會導致無限的 1 流被打印出來。
實際上，它會導致 show (fix (1:)) = "[" ++ intercalate "," (map show (fix (1:))) ++ "]" 的求值，雖然 map show (fix (1:)) 永遠不會完全完成它的工作，但它確實會增量地、逐塊地、每次一個 "1" 地生成輸出。
"[" ++ intercalate "," (map show (fix (1:))) ++ "]"
= "[" ++ intercalate "," (map show (let {x = 1 : x} in x)) ++ "]"
= "[" ++ intercalate "," (map show (let {x = 1 : x} in 1 : x)) ++ "]"
= "[" ++ "1" ++ "," ++ intercalate "," (map show (let {x = 1 : x} in x)) ++ "]"
= "[1," ++ intercalate "," (map show (let {x = 1 : x} in 1 : x)) ++ "]"
= "[1," ++ "1" ++ "," ++ intercalate "," (map show (let {x = 1 : x} in x)) ++ "]"
= "[1,1," ++ intercalate "," (map show (let {x = 1 : x} in 1 : x)) ++ "]"
= "[1,1," ++ "1" ++ "," ++ intercalate "," (map show (let {x = 1 : x} in x)) ++ "]"
= "[1,1,1," ++ intercalate "," (map show (let {x = 1 : x} in 1 : x)) ++ "]"
= ...
這就是惰性求值的工作方式：列印函式不需要在開始列印之前消耗整個輸入字串，它只要可以就立即開始列印。
最後，迭代地計算一個數字的平方根的近似值：
-- fix f = let {x = f x} in x
fix (\next guess tol val -> if abs(guess^2-val) < tol then guess else
next ((guess + val / guess) / 2.0) tol val)
2.0 0.0001 25.0
= (let {rec = (\next guess tol val -> if abs(guess^2-val) < tol then guess else
next ((guess + val / guess) / 2.0) tol val) rec}
in rec) 2.0 0.0001 25.0
= let {rec guess tol val = if abs(guess^2-val) < tol then guess else
rec ((guess + val / guess) / 2.0) tol val}
in rec 2.0 0.0001 25.0
= 5.000000000016778
| 練習 |
|---|
|
以下表達式會收斂到什麼值（如果有的話）？
|
fix 也可以用一種不引入結構共享的方式定義：
fix :: (a -> a) -> a
fix f = -- x where {x = f x}
-- f x where {x = fix f}
f (fix f)
函式 f 的不動點 是一個值 a，使得 f a == a。例如，0 是函式 (* 3) 的不動點，因為 0 * 3 == 0。這就是 fix 名字的由來：它找到函式的最小定義的不動點。（我們很快就會解釋“最小定義”的含義。）對於上面提到的兩個收斂的例子，這一點很容易看出。
const "hello" "hello" = "hello" (1:) [1,1,..] = [1,1,...]
由於不存在這樣的數字 x，使得 2+x == x，所以 fix (2+) 發散也很合理。
| 練習 |
|---|
對於上面練習中你認為 fix f 收斂的每個函式 f，請驗證 fix f 是否找到了一個不動點。 |
事實上，從 fix 的定義來看，它找到一個不動點是顯而易見的。我們只需要將 fix 的方程反過來寫：
f (fix f) = fix f
這正是不動點的定義！因此，似乎 fix 應該總是找到一個不動點。但是，有時 fix 似乎失敗了，因為它有時會發散。然而，如果我們引入一些 語義學，我們可以修復這個屬性。每個 Haskell 型別實際上都包含一個名為底的特殊值，記為 ⊥。因此，例如，型別為 Int 的值實際上包括 ⊥ 以及 1, 2, 3 等。發散的計算用 ⊥ 表示，也就是說，我們有 fix (2+) = ⊥。
特殊值 undefined 也用 ⊥ 表示。現在我們可以理解 fix 如何找到像 (2+) 這樣的函式的不動點。
例子： (2+) 的不動點
Prelude> (2+) undefined *** Exception: Prelude.undefined
因此，將 undefined （即 ⊥）輸入到 (2+) 會得到 undefined。所以 ⊥ 是 (2+) 的不動點！
在 (2+) 的情況下，它是唯一的不動點。然而，還有一些其他函式 f 具有多個不動點，而 fix f 仍然發散：fix (*3) 發散，但我們在上面提到過 0 是該函式的不動點。這就是“最小定義”條款發揮作用的地方。Haskell 中的型別有一個叫做定義度的偏序關係。在任何型別中，⊥ 都是最小定義的值（因此被稱為“底”）。對於像 Int 這樣的簡單型別，偏序關係中唯一的對是 ⊥ ≤ 1、⊥ ≤ 2 等等。對於任何非底的 Int，我們都沒有 m ≤ n。類似的評論適用於其他簡單型別，例如 Bool 和 ()。對於像列表或 Maybe 這樣的“分層”值，情況更加複雜，我們將參考關於語義學 的章節。
因此，由於 ⊥ 是所有型別的最小定義的值，而 fix 找到最小定義的不動點，如果 f ⊥ = ⊥，那麼我們就有 fix f = ⊥（反之亦然）。如果你已經閱讀了語義學文章，你會認出這是一個嚴格函式的標準：當且僅當 f 是嚴格函式時，fix f 發散。
如果你已經遇到過 fix 的例子，很可能是與 fix 和遞迴相關的例子。這是一個經典的例子：
例子： 用 fix 編碼遞迴
Prelude> let fact n = if n == 0 then 1 else n * fact (n-1) in fact 5 120 Prelude> fix (\rec n -> if n == 0 then 1 else n * rec (n-1)) 5 120
這裡我們使用 fix 來“編碼”階乘函式：注意（如果我們將 fix 視為語言原語），我們對 fact 的第二個定義完全不涉及遞迴。在像型別化的 lambda 演算這樣的沒有遞迴特性的語言中，我們可以引入 fix 來用這種方式編寫遞迴函式。這裡還有一些其他例子。
例子： 更多的 fix 例子
Prelude> fix (\rec f l -> if null l then [] else f (head l) : rec f (tail l)) (+1) [1..3] [2,3,4] Prelude> map (fix (\rec n -> if n == 1 || n == 2 then 1 else rec (n-1) + rec (n-2))) [1..10] [1,1,2,3,5,8,13,21,34,55]
那麼，這是如何運作的呢？讓我們首先從語義學的角度來解釋我們的 fact 函式。為了簡潔，我們定義：
fact' rec n = if n == 0 then 1 else n * rec (n-1)
這與上面第一個示例中的函式相同，只是我們給匿名函式命名，以便現在計算的是 fix fact' 5。fix 將找到 fact' 的不動點，即滿足 f == fact' f 的函式 f。但讓我們來擴充套件一下這到底意味著什麼。
f = fact' f = \n -> if n == 0 then 1 else n * f (n-1)
我們所做的只是在 fact' 的定義中用 f 替換 rec。但這看起來完全像階乘函式的遞迴定義！fix fact' 將自身作為第一個引數傳遞給 fact'，從而從高階函式（在舊的 LISP 語法中也稱為函式式）中建立一個遞迴函式，該函式表達了整個遞迴計算的一步。
我們也可以從更操作的角度來考慮問題。讓我們實際擴充套件 fix fact' 的定義。
fix fact'
= fact' (fix fact')
= (\rec n -> if n == 0 then 1 else n * rec (n-1)) (fix fact')
= \n -> if n == 0 then 1 else n * fix fact' (n-1)
= \n -> if n == 0 then 1 else n * fact' (fix fact') (n-1)
= \n -> if n == 0 then 1
else n * (\rec n' -> if n' == 0 then 1 else n' * rec (n'-1)) (fix fact') (n-1)
= \n -> if n == 0 then 1
else n * (if n-1 == 0 then 1 else (n-1) * fix fact' (n-2))
= \n -> if n == 0 then 1
else n * (if n-1 == 0 then 1
else (n-1) * (if n-2 == 0 then 1
else (n-2) * fix fact' (n-3)))
= ...
請注意，使用 fix 使我們能夠不斷“展開” fact' 的定義：每次遇到 else 子句時，我們都會透過評估規則 fix fact' = fact' (fix fact') 生成 fact' 的另一個副本，該規則充當遞迴鏈中的下一個呼叫。最終我們會遇到 then 子句，並從該鏈中退出。
而且，透過將 fix 的共享定義放在本頁頂部，fix fact' 將建立一個實際的遞迴函式，該函式使用自身來進行遞迴呼叫，而不是使用其副本。
fix fact'
= let rec = fact' rec in rec
= let rec = (\rec' n -> if n == 0 then 1 else n * rec' (n-1)) rec in rec
= let rec = (\n -> if n == 0 then 1 else n * rec (n-1)) in rec
= let rec = (\n -> if n == 0 then 1 else n * rec (n-1)) in
\n -> if n == 0 then 1 else n * rec (n-1)
= let rec = (\n -> if n == 0 then 1 else n * rec (n-1)) in
\n -> if n == 0 then 1
else n * (if n-1 == 0 then 1 else (n-1) * rec (n-2))
= ...
這得益於 Haskell 的 let 允許遞迴定義，實際上與 Scheme 的 letrec 在這方面類似。非共享 fix 定義不使用此方法，並且也適用於非遞迴 let - 雖然它本身也是遞迴定義的（此處），但它建立的函式實際上不是自引用的，並且透過重新建立自己的副本並呼叫它來實現遞迴，正如我們上面所見。這就是為什麼在非遞迴語言中新增遞迴的一種方法是將 fix 新增到其中，作為一種基本構造。
fix 的非遞迴定義也存在。其中最簡單、最著名的被稱為Y 組合子。在非型別化 Haskell 中，它可以寫成 y = u . (. u)，其中 u x = x x 被稱為U 組合子。
| 練習 |
|---|
|
型別化 lambda 演算
[edit | edit source]在本節中，我們將擴充套件上一節中多次提到的一個觀點：fix 如何使我們能夠在型別化 lambda 演算中編碼遞迴。它假定你已經瞭解型別化 lambda 演算。回想一下，在 lambda 演算中，沒有 let 子句或頂級繫結。每個程式都是 lambda 抽象、應用和字面量的簡單樹。假設我們想寫一個 fact 函式。假設我們有一個名為 Nat 的型別來表示自然數，我們會從以下類似的內容開始
λn:Nat. if iszero n then 1 else n * <blank> (n-1)
問題是，我們如何填寫 <blank>？我們沒有函式的名稱，因此無法遞迴呼叫它。繫結名稱到項的唯一方法是使用 lambda 抽象，所以讓我們試一試
(λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1)) (λm:Nat. if iszero m then 1 else m * <blank> (m-1))
這擴充套件為
λn:Nat. if iszero n then 1
else n * (if iszero n-1 then 1 else (n-1) * <blank> (n-2))
我們仍然有 <blank>。我們可以嘗試再新增一層
(λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1)
((λg:Nat→Nat. λm:Nat. if iszero m then 1 else m * g (m-1))
(λp:Nat. if iszero p then 1 else p * <blank> (p-1))))
->
λn:Nat. if iszero n then 1
else n * (if iszero n-1 then 1
else (n-1) * (if iszero n-2 then 1 else (n-2) * <blank> (n-3)))
很明顯，無論我們新增多少層命名，我們都無法消除這個 <blank>。除非我們使用 fix，它本質上提供了一個物件，我們可以從中始終展開一層遞迴，並且仍然得到我們開始時的內容。
fix (λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1))
這是型別化 lambda 演算加上 fix 中一個完美的階乘函式。
在型別化 lambda 演算的上下文中，fix 實際上比這更有意思：如果我們將其引入語言中，那麼每種型別都將被填充，因為給定某個具體型別 T，以下表達式具有型別 T
fix (λx:T. x)
這在 Haskell 語言中就是 fix id，它在語義上是 ⊥。因此，我們看到，一旦我們將 fix 引入型別化 lambda 演算中，每個型別良好的項都減少到一個值的屬性就會丟失。
Fix 作為資料型別
[edit | edit source]在 Haskell 中也可以建立 fix 資料型別。
有三種定義方法。
newtype Fix f = Fix (f (Fix f))
或者使用 RankNTypes 擴充套件
newtype Mu f = Mu (forall a . (f a -> a) -> a) data Nu f = forall a . Nu a (a -> f a)
Mu 和 Nu 有助於泛化摺疊、展開和重新摺疊。
fold :: (f a -> a) -> Mu f -> a fold g (Mu f) = f g unfold :: (a -> f a) -> a -> Nu f unfold f x = Nu x f refold :: (a -> f a) -> (g a -> a) -> Mu f -> Nu g refold f g = unfold g . fold f
Mu 和 Nu 是 Fix 的受限版本。Mu 用於建立歸納的非無限資料，而 Nu 用於建立共歸納的無限資料。例如）
newtype Stream a = Stream (Nu ((,) a)) -- exists b . (b, b -> (a, b)) newtype Void a = Void (Mu ((,) a)) -- forall b . ((a, b) -> b) -> b
與不動點函式不同，不動點型別不會導致底部。在以下程式碼中，Bot 被完美地定義。它等效於單元型別 ()。
newtype Id a = Id a newtype Bot = Bot (Fix Id) -- equals newtype Bot=Bot Bot -- There is only one allowable term. Bot $ Bot $ Bot $ Bot ..,
Fix 資料型別不能模擬所有形式的遞迴。例如，這種非正則資料型別。
data Node a = Two a a | Three a a a data FingerTree a = U a | Up (FingerTree (Node a))
使用 Fix 實現它並不容易。