简单类型的Lambda演算

参考资料：Lambda Calculus with Types

给Lambda项增加类型

类似于编程视角下的范畴和函子，我们让变量具有对象的类型，让函数具有箭头的类型。这样，只有函数（箭头的类型）作用于变量（对象的类型）是合法的
简单类型的集合
- （对象）如果 $\alpha \in \mathbb{V}$ ，那么 $\alpha \in \mathbb{T}$
- （箭头）如果 $\sigma$ 、 $\tau \in \mathbb{T}$ ，那么 $\sigma \to \tau \in \mathbb{T}$
Lambda项的类型
- （变量） $x$ 具有唯一的类型 $\sigma \in \mathbb{V}$ ，记为 $x : \sigma$
- （抽象）如果 $x : \sigma$ 、 $M : \tau$ ，那么 $\lambda x.M : \sigma \to \tau$
- （作用）如果 $M : \sigma \to \tau$ 、 $N : \sigma$ ，那么 $MN : \tau$
注意，并非所有Lambda项都具有类型（比如变量作用于变量）。如果一个Lambda项具有类型，那么它称为可类型化的Lambda项