作者：Giuseppe Castagna，巴黎大学
因为这是论文导读啦，所以顺序和原文无关，如果出现了任何错误请第一时间联系我并实际结果以论文为准。
首先说点跟内容无关的，现在的学术人啊，没了unicode的支持写不了两个花里胡哨的符号就写不了代码了是吧，写的我真的好痛苦。
i + i1 + j2 * iji上面第一个例子是我的某个OI朋友写的出来的代码
下面的例子是我的某个朋友写的Agda
现在我们用的大多数的编程语言都会有一个工具 ”类型“ 用来帮助开发，大部分的类型系统的构造都非常的精妙和复杂，但是集合类型理论提供了一套非常简单：正如标题提到的，这个类型系统非常的简单，只需要懂集合论就可以看懂的程度，不过这篇论文带来的启发性远远大于他（目前的）的成果。
在开始讲解之前我们先用ML语法写一个flatten函数，这个函数相信很多玩过fp语言的人都知道长什么样
let rec flatten = function
| [] -> []
| head::tail -> (flatten head)@(flatten tail)
| x -> [x]如果你不幸看不懂这种语法我还贴心的为你准备了类似JS的语法
function flatten(obj){
if(obj.empty()){
return obj
}
if(obj.is_not_list()){
return new List(obj)
}
return flatten(obj.head).concat(flatten(obj.tail))
}那么我们来思考一下他的类型, 结果就是如果你不使用泛型系统（除去元素的类型外）， 你很难去描述他的具体类型。
这里作者假定了一种使用交集和否定的类型系统
$$ type\ Tree(\alpha)\ =\ (\alpha\ \backslash \ List(Any))\ |\ List(Tree(\alpha)) $$我们解释下 ”\“ 的意思是不是（difference）“|” 的意思是包括（union），List(T) 表示装着T类型为元素的表列，然后“&”暂时还没有出场，他是交集的意思。
上边的Tree的类型的意思就是这个Tree里面有个类型α，这个有两种存在的形态
- 不是List(Any也就是任意类型) 的类型
- List里面存在Tree(α)
所以换成人话就是它里面的元素要么是一个叶子（因为不是任意类型的数组），要么是一个子树。
那么这个flatten我们就可以给出这个类型
let rec flatten: ∀α. Tree(α) -> List(α)可能大家到这里没有觉得有什么大不了的，不就是一个泛型和一个类型定义吗。
但是你们看这个Tree的类型的定义有说他真的是树吗？
并没有欸！
也就是其实他这套类型系统是规定了长成这样的形状任何数据结构都可以是树（Tree）。
他其实是规定了一个形状作为类型而并没有使用过多的名称也没有描述过多的行为。
然后我们不是有并集吗，那么在这个编程语言里面我们可以写出非常泛型的代码
let res: List(Int|Bool|String) = flatten [
3, "r", [ 4, [ true, 5] ], [
"whatever", [[ false ], "stop" ]
]
]其实这里作者给出了一个语言可以这么写代码，大家可以去看看这门给XML准备的语言CDuce
有一些读者可能会好奇，咱的否定类型去哪儿了？
这里作者把Bool（布尔值）类型拆成了True类型和False类型。
然后我们可以写一个函数叫 not
let not = fun x -> if x then false else true这里not的类型就非常有意思了
$$ (true \rightarrow false) \& (false \rightarrow true) $$熟悉布尔运算的朋友就可以立马反应过来！哦我知道，他把布尔运算提升到了类型的高度了！
然后就能写出and和or
let and = fun x y ->
if x then (if y then true else false) else false
// 大家应该都知道这个规则的吧...
let or = func x y ->
not (and (not x) (not y))我们可以写出他们的类型（其实对于一般的编程语言并不是非常好描述布尔运算的类型因为if多半是build in的东西而true和false是bool类型的，这个论文这么做有他独特的理由，但这里空间太小了，还是去看原论文来的实在。
$$ and:\ (false \rightarrow false) \& (\lnot false \rightarrow ((\lnot false \rightarrow true)\&(false \rightarrow false))) \\ or:\ (\lnot false \rightarrow Any \rightarrow true) \& (false \rightarrow ((\lnot false \rightarrow true) \& (false \rightarrow false))) $$使用这套类型系统我们可以完成三种多态
- Parametric：参数多态也就是平常人说的泛型参数
- Ad-hoc： 也就是正常人说的允许运算符重载
- Subtype：也就是正常Jawa人说的OOP
那么最后就是作者举得一个非常厉害的例子：红黑树
这套类型系统可以描述树的平衡和不平衡。
type RBTree(a) = BlackTree(a) | RedTree(a)
type RedTree(a) = (Red, a, BlackTree(a), BlackTree(a))
type BlackTree(a) = (Black, a, RBTree(a), RBTree(a)) | Leaf
// 偏移的子树
type WrongTree(a) = (Red, a, RedTree(a), BlackTree(a)) |
(Red, a, BlackTree(a), RedTree(a))
// 不平衡的树
type Unbalanced(a) = (Black, a, WrongTree(a), RBTree(a)) |
(Black, a, RBTree(a), WrongTree(a))这套类型推导相当的慢，但是我懒得算复杂度了，反正肯定是指数爆炸级别的慢，但是作者在论文里指出了一点点优化方针，后面的内容就是相机是之类的和推到规则之类的了，我也就不搬运了，总之我们可以看到这套类型系统很简单但是很强大。
顺带一提：这篇论文可能是写给TypedRacket的，我们可以期待一下看看近期他写完会不会出库给我们试用。
