※ 引述《noctem (noctem)》之铭言：
: 解释得很棒！真是感谢...
: ※ 引述《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.
_|_ (\bot) 是任意 type 的 proof term 是什么意思呢？
_|_ 应该是对应 logic 上的 false 或称 absurdity,
虽然 \bot 也用在 denotational semantics 上, 作为
information order 上"没有资讯"的意思，也就是最小元素，
而 Haskell 也用这个作为所有 type 的 term，因此可以说 Haskell 是
不一致的系统。若用 Heyting algebra 来看 logic 的话，
_|_ 的确也是最小元素。
但这两个 \bot 还是不同吧？
: 补充一下，这里操作上的意思是我们能写出不会中断的程式。
: 用 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）。
虽然是这样说，不过其实可以设计一个给 domain 的逻辑系统，
有语意，语法以及对应的sequent calculus, 这角度来看就算有 \bot
还是 consistent 的啦。
: : 不过写了这么多都没提到 Kind.
: 其实我是不太知道 kind 在这边的意义哩。说说看吧？
: : (Note: 这段对 user defined data type 的解释很狭隘, 仅限之后够用而已,
: : data type 的理论 Robert Harper 还在写的新书里写了整整两章)
: 喔喔，这个有草稿可以抓吗？
: （其实回这篇是为了要问这个 XD）
既然说到这个，我一直想说 FP 对应的逻辑都是构造性的，
但是 wiki 看到的资料写, 加入 Call-with-current-continuation
对应 Peirce's law 就会是古典逻辑了。但我不晓得实际拿来作证明，
会长什么样子呢？