Re: [心得] Y Combinator 與 Mutual Recursion

看板PLT (程式語言與理論)作者scwg ( )時間14年前 (2010/06/04 12:49)推噓0(0推 0噓 0→)

留言0則, 0人參與討論串3/6 (看更多)

※ 引述《SansWord (是妳)》之銘言： : : 解決方法也很簡單，就頭痛醫頭腳痛醫腳，做一個 t 與 t -> a : : 同構的遞迴型別囉。 : : data Fix a = Rec (Fix a -> a) -- Fix a 和 Fix a -> a 同構老實說你的問題真是戳在痛處.. 讀了那麼久 type system 還沒好好想過這個問題下面來試著回答看看首先先確定一個概念: function 也是 data, 只不過一般的 data type 是 Int function 的 type 會是 Int -> Int 因此 value-type-kind 的三層結構裡, function 和 data 同在最底層的 value 裡因此 "data 層次的 recursive" 一樣會遇到問題, 就你早先提到的 (letrec ((x (* y 2)), (y (/ z 3)), (z (+ x 1))) (+ x y z)) 在 haskell 裡是寫成 let x = y * 2 y = z / 3 z = x + 1 in x + y + z 如果不用語言本身給的 mutual recursive, 就一樣要用 Y 加上 triple 來定義 (e.g. let (x, y, z) = Y (\(x', y', z') -> (y'*2, z'/3, x'+1)) in x + y + z 不過這樣不 work, 原因請參考 ccshan 在本板的最後一篇文章) 回到正題. data 和 type 是什麼? data 當然就是一些 "物體", type 則是描述 "這個物體能做什麼". 3 是一個 "物體", Int 告訴我們 "他可以用在 peano arithmetic 的敘束裡" (\x -> x + 1) 是一個 "物體", Int -> Int 告訴我們 "他可以把 Int 轉換成 Int" 這是常見的解釋. 另一方面, Curry-Howard correspondence 告訴我們, type 是 logic proposition "a -> a" 是 "若 a 則 a", 而 (\x -> x) 則是 "若 a 則 a 的證明" 也就是說: data 是證明, 有時候叫 "proof term", type 則是 logic proposition. 那麼 type inference 是什麼? W-algorithm 在做什麼? Unification 又是什麼? type inference 是從 data 反推 type, 也就是從證明出發, 找出在證什麼 W-algorithm 就是檢查所有可能的證明步驟 Unification 是在說: "現在看起來這個 proof term 你既用來證第一個 proposition, 又用來證第二個 proposition, 那麼要不這兩件事是同一件事 ( unify (a :-> b) (c :-> d) = unify a c +++ unify b d ) 要不某個 proposition 不能太 general, 只能是特定形式 ( unify (Var a) e = a |-> e where e /= (Var a) )" 之所以要導入 Fix 是因為定義 Y 的時候用到了 (\x -> f (x x)) ... W-algorithm 看到 x x 這個證明就說, 這是個 application, 所以前半是某個 t -> a 的證明, 後半是 t 的證明, 兩個合起來就證了 a. 於是給了前半的 x :: t -> a, 後半的 x :: t, 再來 unify: t -> a = t Unification 就生氣了: 你說這個證明證了 t 又證了從 t 可以得到任意 a 那不是光你自己就可以證出所有的 a 了? 更一般地來說, unify (Var a) e = a |-> e 的時候, e 裡面不能包涵 a, 否則這個 type check is unsound. 無論再怎麼增強我們的 type system, 這個 Y 就是沒辦法 type check. 於是 noctem 就拿出了秘密武器: user defined data type. 在 Curry-Howard correspondence 底下 user defined data type 應該是什麼了? (Note: 這段對 user defined data type 的解釋很狹隘, 僅限之後夠用而已, data type 的理論 Robert Harper 還在寫的新書裡寫了整整兩章) data Fix a = .... 接受一個 type (proposition), 變成另一個 type (proposition) 因此 Fix 是個 predicate! data Fix a = Rec (Fix a -> a) 那 Rec 是什麼呢? 給他一個 (Fix a -> a) 的 value (proof), 他會給我們一個 (Fix a) 的 value (proof) 因此 Rec 是 Axiom! 經由這個 axiom, 我們才能證明剛剛新定義的 predicate Fix. 這個 Axiom 則很妙, 他只要求一個 "Fix a 可以推出 a" 的證明就聲稱可以證明 "Fix a" 很明顯這個一點都不通. 但是這就是 False value _|_ (bottom) 的來源. 那麼稍微修改後, 不太對稱但可以 type check 的 Y 成了 Y = (\(Rec x) -> f (x (Rec x))) (Rec (\(Rec x) -> f (x (Rec x)))) 在適當的時候用 Rec 這個 Axiom 來把 x 這個 t -> a 的證明變成 t 的證明, 世界真美好. 這麼一來我們可以寫 recursive program 了, 不過有什麼損失嗎? 有的. 在沒有 Y 之前的 typed lambda calculus 是沒有 divergence 的. 所有的 function 都是 total function, 給了 input 一定有 output. 但是 recursive 給了我們造出 divergence 的空間, function 不一定是 total 了. 事實上這表示我們證得出 "False" 了! 因為 _|_ 是任何 type 的 proof term. 這個 logic 不再 consistent, proof term 不再是 valid proof. 不過一般在寫程式, 表達能力當然重要得多. 不是 Turing complete 的 language 寫起來常常礙手礙腳. 但是在一些 proof assistant 裡, 因為主要功能就是證明, 所以上面的 Fix 通常是不合法的. 要 recursive 可以, 通常只給 primitive recursion, 這樣還是只寫得出 total function, logic is still consistent. == 不過寫了這麼多都沒提到 Kind. 就先當 "type checking logic proposition" 吧 XD : 這邊有個疑問 : 在Function 裡面定義recursive function 會有問題～ : 所以用Y combinator 可以搞定～ : 那為什麼 : data 層次的recursive 定義不會遇到類似的問題? : 這與haskell的什麼語言特性有關嗎？ : 是否有些語言可以支援這樣的宣告，有些卻不行? 若是如此，差別又在哪裡？ : 似乎有點鑽牛角尖了....^^" 不過我對haskell 中 data 和type 的互動的概念有點模糊 : == : 不過我好像隱隱約約可以回答這個問題～ : 這樣的語法是Type Constructor宣告 : 看似會有狀況，不過只要導入 Kind 的概念，則 : Fix:: * -> * (這邊正確嗎？我這裡還沒有很清楚) : 就能夠順利的用 W-Alogorithm 做 Unification : 也就可以順利的進行 Type Inference? : == : 會打問號是因為我沒辦法很肯定自己的回答是否正確～ : 目前正處於念了一些書可是還在相互整合的階段.... -- All this will not be finished in the first 100 days. Nor will it be finished in the first 1,000 days, nor in the life of this Administration, nor even perhaps in our lifetime on this planet. But let us begin. -- John F. Kennedy, Inaugural Address -- ※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 128.36.229.73