※ 引述《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