基本类型 Base Types
用 A B C 表示基本类型 base types / atomic types 名称，$ A $ 表示基本类型组成的集合
当展示求值的结果时，将省略 λ 抽象体，直接简记为一个 <fun>，比如
λx : B . x
> <fun> : B → B
单位类型 Unit Types
Unit 类型的成员只有 unit
Derived forms 在下一节
Unit 在带副作用的语言中有很重要的作用；主要应用在带副作用的操作的语句（例如赋值语句）
导出形式：序列
对序列中的两个或者多个表达式求值 t1; t2，求值 t1 然后丢掉结果求值 t2
有两种方法去规范地定义序列
The high-level typing and evaluation rules for sequencing can be derived from the abbreviation of t1;t2 as (λx:Unit.t2) t1. This intuitive correspondence is captured more formally by arguing that typing and evaluation both “commute” with the expansion of the abbreviation.
也就是说序列的更高级的类型化和运算可以从后面这个 lambda 形式导出
定理：
The advantage of introducing features like sequencing as derived forms rather than as full-fledged language constructs is that we can extend the surface syntax (i.e., the language that the programmer actually uses to write programs) without adding any complexity to the internal language about which theorems such as type safety must be proved.
我们可以扩展表面语法而不使语法的内核复杂化
通配符
Another derived form that will be useful in examples later on is the “wild-card” convention for variable binders. It often happens (for example, in terms created by desugaring sequencing) that we want to write a “dummy” lambda-abstraction in which the parameter variable is not actually used in the body of the abstraction. In such cases, it is annoying to have to explicitly choose a name for the bound variable; instead, we would like to replace it by a wildcard binder, written _. That is, we will write λ_:S.t to abbreviate λx:S.t, where x is some variable not occurring in t.
之前我们写出了一个虚拟的 λ，而囿变量 x 是一个实际上并不在抽象体中的变量，这个时候我们用通配符 _ 指代这种参数变量
归属
用 t as T 将一种类型 T 归属到给定的项 t
The typing rule T-Ascribe for this construct (cf. Figure 11-3) simply verifies that the ascribed type T is, indeed, the type of t. The evaluation rule E-Ascribe is equally straightforward: it just throws away the ascription, leaving t free to evaluate as usual.
归属的作用有：
-
documentation使程序容易阅读 -
让复杂类型便于编写（一种缩写机制），比如：
UU = Unit → Unit
UU 表示 Unit → Unit 的一个缩写
(λf : UU . f unit)(λx : unit . x)
- 抽象机制
abstraction
let 绑定
在 OCaml 中已经见过，let 给表达式绑定一个名称；let x = t1 in t2 表示对 t1 求值，在计算 t2 时把 x 绑定为 t1 的结果
let 也可以被表示成一个导出形式：
But notice that the right-hand side of this abbreviation includes the type annotation T1, which does not appear on the left-hand side.
等式左边并不包含 T1 这个类型信息而右边包含
_We discover the needed type annotation simply by calculating the type of t1.
意味着我们要通过类型推断得到 t1 的类型
More formally, what this tells us is that the let constructor is a slightly different sort of derived form than the ones we have seen up till now: we should regard it not as a desugaring transformation on terms, but as a transformation on typing derivations (or, if you prefer, on terms decorated by the typechecker with the results of its analysis) that maps a derivation involving let.
形式上的解释是，let 的导出形式与目前所有的已知的导出形式不同，不是项上的转换，而是类型推导的一个转换：
序偶
注意隐含的求值顺序（从左到右）
元组
