函数类型
因为纯粹的 lambda 演算是 turing 完备的，因此只有运行时才能够完全确定类型，比如：
if <complex evaluation> then true else (λx.x)
定义函数类型：λx.t: →；为了更加精确，加入参数 T1 T2，得到如下递归定义：
定义：类型 Bool 上的简单类型集合是由下列语法产生的：
T ::=
Bool (布尔类型)
T → T （函数类型）
类型构造子是右结合的，即 T1 → T2 → T3 ≡ T1 → (T2 → T3)，这也与直觉相吻合
类型关系
首先遇到的问题是：对于一个 abstraction，怎么知道参数是什么类型？
-
给参数添加类型注释（相当于给参数指派一个类型）；称为显式类型化
explicitly typed -
分析抽象体，通过体中囿变量的行为逆推断参数类型；称为隐式类型化
implicitly typed
TaPL 集中讨论第一种方案
既然已知参数类型，那么函数结果的类型显然是抽象体的类型，表示为：
原来这里自带图床
类型上下文 typing context
由于项 x 可能包含 lambda 抽象，所以为了保证推导的准确性，需要若干个同样的类型注释（也可以理解成一个指派 / 假设），因此我们拓展一下类型关系，添加一个类型上下文 typing context，记为 Γ；原先 t : T 的类型关系被扩展为 Γ ├ t : T 的一个三元关系；同时 comma 算子 , 被用来扩展 Γ，比如：Γ , x : T 意味着新的绑定 binding 被加入了这个上下文之中，Γ 可以看作从变量到类型的一个函数
\(\lambda_\rightarrow\) 称为简单类型的 lambda 演算
类型的性质 Properties
引理：（类型关系的逆）
