类型系统的根本目的是防止程序运行过程中出现执行错误，这个非正式的声明激发了对类型系统的研究。它的准确性首先取决于一个相当微妙的问题——什么是执行错误。然而即使解决了这个问题，没有执行错误也是一个相当不简单的性质。我们必须证明所有可以在编程语言中表达的程序都没有执行错误，才能说该语言是类型安全的。（注：原文是 type soundness，译为类型健全；我们使用了更通俗的术语 type safety，即 “类型安全”。）事实证明，在进行相当多的仔细分析后，才可能避免对编程语言的类型健全性提出错误或令人尴尬的声明。而类型系统的分类、描述和研究也已经成为一门正式的学科。
在程序的执行过程中，一个程序变量可以承担一定的数值（数据）范围。这种范围的上限被称为该变量的类型。例如，一个布尔类型的变量 x 应该在程序的每次运行中只承担布尔值。如果 x 是布尔类型，那么布尔表达式 not(x) 在程序的每次运行中都有合理的意义；如果 x 承载了布尔以外的值，例如字符串，那么布尔表达式 not(x) 并无合理的意义。
类型化语言和非类型化语言
变量可以被赋予非平凡的（即非单一通用类型）类型的语言被称为类型化语言。（原文为 typed languages 和 untyped languages，直译为“类型化的语言”和“非类型化的语言”，译者注。）
实现安全所需的运行时检查有时被认为太昂贵（例如即使在有大量静态分析的语言中，数组越界等检查通常也不能在编译时完全消除），因此出于性能考虑，有些语言被故意做成不安全的，例如 C 语言。尽管如此，仍有许多人在努力设计安全的 C 语言子集，并制作开发工具，试图通过引入各种（相对昂贵的）运行时检查来安全地执行 C 程序。这些努力来自两个主要的原因：
C 语言也被广泛使用在那些对性能要求不高的应用中，
不安全的 C 语言程序所带来安全问题，例如缓冲区溢出和算术下溢，可能导致覆盖任意的内存区域，并可被利用进行攻击。
像 Pascal 这样的显式类型的程序性语言的类型推断问题是相当容易解决的，隐式类型语言如 ML 的类型推断问题要微妙得多：而在多态（polymorphism）存在的情况下，类型推断问题变得特别困难。Ada 和 Standard ML 的显式类型多态结构的类型推断问题在实践中是可以处理的；然而，这些问题基本上是由算法解决的，而没有描述它们的类型系统。适用于多态的最纯粹和一般的类型系统是由 λ-演算给出的（之后介绍）。
序一：本来打算写“浅谈 Intersection Types 和 Union Types”的，后来考虑到前者的篇幅已经有点长了，就砍成了“浅谈 Intersection Types”，后半部分以后再谈。
序二：网上其实有挺多关于 intersection types （和 union types）的文章了，且大部分是以 TypeScript 为宿主语言进行说明的。不过那些文章比较侧重这两种类型在 TypeScript 中的使用方式，对这以外的知识鲜有说明，本文旨在弥补这一不足。
本文大量参考了《Programming with Intersection Types and Bounded Polymorphism》《Row and Bounded Polymorphism via Disjoint Polymorphism》，或者直接说翻译吧，更贴切些，毕竟也没有太多自己的原创研究。
如上的 Java 代码， T extends Fly & Swim & Run 部分引入的类型 T 本质上就是一个 I 类型 ，意即 T “既要能飞，且要会游，还要善跑”。可以看出，在函数 test 函数中，T 类型的 omni 确实展现出了惊动自然的能力，先后表演了飞翔、潜泳、疾驰，最后连跑带飞的溜了。刚开始介绍，不要嫌我啰嗦：“所以说，正因为 T 这个类型兼具了 Fly、Swim、Run 三个类型的所有能力，定义在这三个类型里的函数才都可以被调用；如果这三个类型有成员的话，自然也都是可以被访问的。”
我们不禁要问，这样的传奇真的存在吗？还好，在代码中我们可以直接无中生有，例如
1 2 3 4 5
classOmnipotenceimplementsFly, Swim, Run { voidswim() { /* do something */ }; voidrun() { /* do something */ }; voidfly() { /* do something */ }; }
便硬生生地造了一个满足要求的类型 Omnipotence，对造物主来说真是小事一桩。
言归正传。下文中我们使用 & 作为 I 类型的类型构造器。& 接受两个类型（其实一组类型也可以，但本文想尽量简单些），并构造出单个 I 类型：
1
& : (Type, Type) -> Type // 意会一下，我们就不引入 kind 的概念了
上文中 T 的类型可表示为 T : Fly & Swim & Run。
& 像加法一样具有结合律，所以实现的时候不太需要关注它到底是左结合的还是右结合的，随意啦。
如果还是觉得不好理解的话，不妨回想一下函数类型 T -> R，我们可以说 -> 是函数类型的类型构造器
如果同一个作用域下的函数 f 定义了好几次且构成重载，那么 f 具有什么类型呢？我想聪明的读者应该已经想到了，很明显，f 可以具有 I 类型。
1 2
f : Int -> Int f : Double -> Double
我们不妨把 f 的类型写成 Int -> Int & Double -> Double。为了少写几个括号，我们假设 -> 的结合性比 & 更强。
这样的 f，既可以处理整数，也可以处理浮点数，因此 f(1) （假设 1 不符合浮点数语法）与 f(1.0) 均为合法的调用——前者选用 Int -> Int 的逻辑处理，后者选用 Double -> Double 的逻辑处理 。
如果再给 f 新增一个能处理布尔类型的定义
1
f : Bool -> Bool
那么函数调用 f(true) 也将是合法的，此时 f 的类型将变成 Int -> Int & Double -> Double & Bool -> Bool。
那么 I 类型可以替代重载吗？我认为取决于需求。
I 类型的类型检查与非确定行为
根据《Programming with Intersection Types and Bounded Polymorphism》，I 类型的类型检查会“穷尽每一种可能”。在做函数调用 f(t)时，如果 f 和 t 都是 I 类型，那么每一组可以“匹配”的类型都会产生一个结果类型；如果“匹配”的类型超过一个，那么函数调用的结果类型仍然是一个 I 类型，例如：
1 2 3 4
f : Bool -> Bool & Bool -> Int t : Bool
f(t) : Bool & Int
因为 f 的 Bool -> Bool 部分和 Bool -> Int 部分都可调用，所以它们会分别接受参数 t 并且生成结果。生成的结果亦使用 & 相连组成一个 I 类型。
这里便可以看出传统的 I 类型检查中的函数调用与常见的函数重载的不同了：函数重载会根据参数类型选取一个特定的、在某种条件下“最优”的 f 类型，如果无法选取则报错——例如此例中，没有其他更多信息时 f(t) 这个调用是要报类型错误的，而 I 类型会枚举并尝试每一种可能。
下面再看另一个例子，加深对 I 类型的函数调用的理解：
1 2 3 4
f : Bool -> Bool & Int -> Int & Double -> Double t : Bool & Int
