解释得很棒！真是感谢... ※ 引述《scwg ( )》之铭言： : 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) )" 这个讲法不错（笔记）。 : 在没有 Y 之前的 typed lambda calculus 是没有 divergence 的. : 所有的 function 都是 total function, 给了 input 一定有 output. : 但是 recursive 给了我们造出 divergence 的空间, function 不一定是 total 了. : 事实上这表示我们证得出 "False" 了! 因为 _|_ 是任何 type 的 proof term. : 这个 logic 不再 consistent, proof term 不再是 valid proof. 补充一下，这里操作上的意思是我们能写出不会中断的程式。 用 untyped lambda calculus 我们能写出可以一直 reduce 下去， 不会终止的 term (例如 Y, 和很多其他的). 它的表达能力和 Turing machine 一样。 加上 type 的 lambda calculus 通常有 strong normalisation 的 性质: 任何 reduction 都会停在某个 normal form. 也就是说用 它来写程式的话，可以确定所有程式都会终止。这样听起来很好， 代价则是可以写的程式变少了（但，有人似乎是认为这样也够了， 详後述），这语言不再是 Turing complete 了。 那个用 Fix 的做法则是用了 type system 开的後门，让我们又可以 定义 Y combinator. 但这麽一来优缺点又颠倒了：你开始可以写 不会中断，有任何 type 的程式，例如 "y id". : 但是在一些 proof assistant 里, 因为主要功能就是证明, : 所以上面的 Fix 通常是不合法的. : 要 recursive 可以, 通常只给 primitive recursion, : 这样还是只写得出 total function, logic is still consistent. 其实应该比 primitive recursion 强一点（欸，其实是很多）啦。 前面的推文有说到 fold/cata, 所以我想这边可以提一下.. 用 System F 就可以模拟 inductive type 了，做法和 Church encoding 一样，一个 type 就是它的 fold. (有我不认识的人到现在还知道我在说什麽吗？ 那就应该认识一下了 XD) 另外也可以模拟 coinductive type, 例如无限长的 list 或 tree, 基本上一个 coinductive type 就直接用它的 unfold 来表示。 这样你就有了一个语言，有 inductive type (可以做 fold), 也有 coinductive type (可以 unfold), 但是 unfold 出来的 东西和 fold 吃的东西的 type 不一样，因此不能做 hylomoprhism. 这样一来所有程式都还是会终止的。 现在大多 proof assistant 只要能表达 second-order logic 就可以这样做。有人是认为这样就很够了。只是你每写一个长得 比较奇怪的程式，就得付一个它会终止的证明（这个证明当然就 表达成某个 inductive type）。 : 不过写了这麽多都没提到 Kind. 其实我是不太知道 kind 在这边的意义哩。说说看吧？ : (Note: 这段对 user defined data type 的解释很狭隘, 仅限之後够用而已, : data type 的理论 Robert Harper 还在写的新书里写了整整两章) 喔喔，这个有草稿可以抓吗？ （其实回这篇是为了要问这个 XD） --

※ 发信站: 批踢踢实业坊(ptt.cc) ◆ From: 140.109.20.217