推 scwg: On Harper's home page, "Practical Foundation for PL" 06/05 02:16
解釋得很棒！真是感謝...
※ 引述《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