NOTE: 集合類型論 -- 差集類型

今天我想介紹一篇論文 Programming with union, intersection, and negation types* 其中差集類型的概念，而紀錄下這篇文章。 我們已經很習慣各式各樣的 polymorphism 了。例如 Parametric polymorphism 說我們可以引入型別變數，呼叫函數的時候時實例化一個適當的型別。 此論文不考慮 prenex form 以外的情況，顯然是因為 ∀\forall∀/∃\exists∃ 要是能到處出現，就能建構不是集合的 type（參見依值類型論）。 在講述差集之前，我們先複習一下 Curry-Howard correspondence 跟 Intuitionistic Type Theory

此論文底下假定型別都是集合，且對任意值 aaa 來說 a:aa : aa:a，於是聯集與交集值也是一個集合/型別。 也因為這些型別都是集合，所以 ¬A\neg A¬A 具有特別的意義，是指除了 AAA 這個型別都可以。 此系統與 Polymorphism 沒有衝突，因此以下也會出現他們的結合。

現在考慮一個常見的結構 tree，我們經常定義

data Tree a
  = Nil
  | Node a [Tree a]

但顯見此樹是同質資料結構，要是我們想要異質資料結構就不是那麼容易定義了。 此論文提出的 set-theoretic type 可以維持相當類似的定義，而不用大費周章。

所以我們的節點要嘛是葉節點（藉由排除任何 ListListList），要嘛就是 tree（一定是 ListListList）。 差集類型的定義如下：

另外這個定義沒有限制沒有任何子樹的 branches 的情況。 舉一個例子看看？

[3 "r" true]

我們可以想像一下 aaa 的 unification 過程：

1. List(Tree(a)) 逐一推導底下元素表達式的型別，跟 Tree(a) unify
2. a 跟 3 合一，由於 Int 不是 List(Any)，於是我們得出 Tree(Int)
3. a=Int 跟 "r" 合一，由於 Int∧¬List(Any)Int \land \neg List(Any)Int∧¬List(Any) 的規則我們得出 Int∧StringInt \land StringInt∧String，於是得出 Tree(Int|String)
4. a=Int|String 跟 true 合一，同上用 ∖\setminus∖ 推理可以得出 Tree(Int|String|Bool)

這裡好玩的地方是這本來需要

• 強制 a 只能想辦法合出 union type（我不知道有誰真的選這個方案）
• 或是拒絕跟新的具體型別合一成功（如 Haskell 等）

現在可以用 ∖\setminus∖ 去控制。不過要是我們寫出

let rec flatten = function
| [] -> []
| h::t -> (flatten h)@(flatten t)
| x -> [x]

這種程式，型別推論應該是得不出 flatten [8 [[3 "r"] true] false] 這種程式要怎麼辦，因為能合成的型別有點多。 不過只要標記說型別是 Tree(a) -> List(a) 就可以把 Tree(a) 導出的 a 傳過來。

作者接下來轉入一些更精細的推導器，比如替以下程式導出 (true -> false ) & (false -> true)

not true  = false
not false = true

但由於這個例子有點太小，我暫時沒有想深入作者關於這部分的論文 XD。 目前這個型別系統還處在初始階段，需要花更多時間去驗證它的每個角落

• 已知推導速度很慢，除非開發者願意幫所有函數寫型別標記
• 容易異質化容器，也就很容易遇到 dynamic typed 常遇到的最佳化障礙