Abstract
Type system的基本目的是防止在程序运行时发生execution error。这种Informal statement非形式化描述有很多内涵：首先该如何严格定义execution error；其次在这种定义下，描述absence of execution error也是Type system很nontrivial的性质——当PL .aka. programming language的所有运行时行为都能确保这种性质的话，我们就说该语言是type sound的。事实证明为了更加没有歧义的描述PL的type soundness，需要做大量的分析和证明。因此针对Type system的分类，描述和研究过程逐渐演变成为一套formal discipline即形式化体系。 \[
\frac{\Gamma_{1} \vdash \Im_{1} ... \Gamma_{n} \vdash \Im_{n}}{\Gamma \vdash \Im}
\]
The formalization of Type system需要一套精确的符号和定义系统，一个严格正确的Type system可以对语言定义的各个重要性质进行完整的判断。而非形式化的描述甚至做不到完整概括语言的type structure则更谈不上实现上的唯一性。比如不同的编译器对于同一套语言Type system的实现往往不尽相同，甚至有一些type unsound的语言定义导致一段代码明明通过typechecker的检查但在运行时奔溃掉。理想情况下我们说formal Type system应该是所有typed programming languages内核定义的一部分。这样的话，typechecking算法就可以严格按照精确的类型spec执行，从某种程度上该语言可以看成是Type sound的。
Introduction
Execution errors
比较典型的execution error就是系统出现了意外的software faults比如illegal instruction fault或者illegal memory reference fault等。但是也存在execution error会没有预兆的发生从而导致数据错误。进一步的还存在像divide by zero，或者derferencing nil等Type system无法避免的sofeware faults。但是有的语言虽然没有Type system却也不会发生software faults。
safety
首先对execution errors进行分类：
trapped errors:导致计算行为瞬间奔溃停止- 除零错误
- 内存非法访问
untrapped errors:刚开始不会很明显，但是后续会导致任意错误- 没有运行时边界检查的数组越界
- 引用错误地址
A program fragment is safe if it does not cause untrapped errors to occur.
所有程序都是safe的语言称为safe languages——因此safe languages是要能排除一切潜在错误。untyped languages通过runtime checks来达到safety——typed languages通过static静态(比如编译期)排除一切潜在错误行为来达到safety，其也可以同时采用runtime和static检查。
well-behaved
针对通用编程语言，我们应该提炼出execution errors的一个子集作为forbidden errors。这个子集应该包含所有的untrapped errors，以及一部分trapped errors。
A program fragment is said to have good behavior/well-behaved, if it doesn't cause any forbidden error to occur.
对比一下safe和well-behaved的定义就可以发现well-behaved的代码是safe的，但反之不然。所有代码都是well-behaved的语言被称为strongly checked。针对一个Strongly checked的语言的特征：
- 不会出现
untrapped errors（safe的保证） - 不会出现包含在
forbidden errors中的部分trapped errors - 其余的
trapped errors发生也只会由于程序员的自身问题导致
Typed languages通过运行静态检查(比如编译期)来实现语言的well-behaved——这样的语言被称为是staticlly checked，整个检查过程被称为typechecking，执行该检查过程的算法被称为type-checker。一段经过type-checker检查的程序被称为well-typed。staticlly checked languages有ML,Java,Pascal等。
Untyped languages通过运行时检查runtime checks来排除所有的forbidden errors。比如它们会检查所有数组边界，所有除法操作，并在错误出现的时候触发异常。整个检查过程被称为dynamic checking。LISP就是这样一门语言，这样的语言尽管没有静态检查，没有类型系统，但却还是strongly checked。
safety or Performance
type system的首要目标就是要通过排除所有程序运行时的untrapped errors来确保程序的safety。但是实际上很多静态语言都不能保证safety——它们的类型系统并没有完全排除掉运行时的untrapped errors。这些语言被称为是weakly-typed，而且其程度都各自不同。C在pointer arithmetic和casting上有大量unsafe的操作。
大多数untyped languages都是completely safe的，否则程序既没有编译期检查又没有运行时检查一旦出错后果不堪设想。比如Assembly就属于这种语言范畴。
| Typed | Untyped | |
|---|---|---|
| Safe | ML、Java | LISP |
| Unsafe | C | Assembly |
但程序语言的safety属性一般需要以牺牲性能为代价。但是究其优势：可以通过引入garbage collection来确保运行时结构的完整，最后其对于像OS/web browsers等应用的安全提供了保证。
那实现safety是通过类型系统即静态还是运行时即动态:
untyped languages会导致大量safety问题untyped languages比如LISP要比weakly-typed languages比如C更难维护
Typed and untyped languages
程序变量在程序运行期间可以假定一系列的值。
An upper bound of such a range is called a type of the variable.
该变量的一个类型就是其值的一个upper bound。比如一个Boolean类型的变量在程序运行过程中只能是true/false，而not(x)在运行时也是有意义的。一门所有变量都有nontrivial types的语言称为typed languages。而没有限制变量范围的语言称为untyped languages——其变量没有type，或者说其变量都有一个universal type。
Type system是type languages的核心部分，用来跟踪types of variables，更普遍的用来跟踪types of expression。只有遵守type system的代码才可以成为该type language的合格程序。而type system可能不会在语言的语法中显式出现。
Type systems are used to determine whether programs are well behaved.
Explicitly typed:types是语法的一部分implicitly typed:types不会显式出现在语法中
properties of type systems
我们在这里假设程序语言需要即safe又type，因此引入type system的讨论。
Types，作为程序语言的一部分有着和其他program annotations编程标记更加实用的特征。总体上来说，对于程序语言行为的annotations涵盖了informal comments，formal spec，甚至theorem proving等。而Types就在几个范畴的中心地带——其比comments更加精确，但是比formal spec更加简洁和易用。总体来讲type system有如下属性：
decidably verifiable:需要有算法(指的是typechecker)来确保程序是well-behaved的。type system的目的不仅仅是描述开发者的意图，更重要的是为了捕捉程序运行时错误。（formal spec只能进行描述）transparent:开发者对于typechecker的行为应该很易于上手。比如很容易看出某段代码是否可以通过类型测试，如果没有通过则问题一定是开发者自身（automatic theorem proving相比之下更晦涩难懂）enforceable:type declarations应该被尽可能的完成静态/动态检查。类型声明和其对应程序之间的一致性应该符合验证。（comments无法做到这一点）
How type systems are formalized
我们如何保证well-typed的程序确实是well-behaved的呢？
这里的
well-typed指的是通过人为设计的类型系统算法typechecker，而well-behaved指的是在运行时不会出现forbidden errors。
Formal type systems就是在PL文档中对type system非形式化描述背后的数学特征描述。一旦某一个type system被形式化了，我们只需证明以下soundness theorem：
Well-typed programs are well-behaved.
一旦该定理成立，我们就说该type system是sound的。
Good behavior of all programs of a typed language and soundness of its type system mean the same thing.
type and term
为了形式化一门程序语言的type system并且证明soundness theorem，就需要在本质上将整个语言都形式化。首先要做的就是描述该语言的语法syntax。对于大多数语言来说这就意味着描述其types and terms的语法。
Types描述程序的静态行为Terms(statements, expressions, and other program fragments)描述算法的行为
scoping rules
下一步是定义语言的scoping规则——该规则明确定义了标识符的作用域即标识符binding locations声明处和occurrences使用处的联系。Typed languages需要这种scoping是静态的，换句话讲就是说标识符的声明binding locations一定要在运行时之前。而标识符的声明处binding locations往往是由语言语法决定的，因此static scoping也叫做lexical scoping。与之相反的就是dynamic scoping。
Scoping can be formally specified by defining the set of free variables of a program fragment (which involves specifying how variables are bound by declarations). The associated notion of substitution of types or terms for free variables can then be defined.
对于作用域的形式化可以定义一个program fragment的一系列free variable,接着可以定义如何使用types/terms来替换这些变量。
- scoping rules, binding locations, free variable
type rules
当这些搞定后，开始定义程序语言的type rules：其通过M:A的形式定义了terms M和types A之间的一种has-type关系。有些语言还通过A<:B的形式定义types之间的subtype-of关系，还有通过A=B的形式定义types之间的equal-type关系。
The collection of type rules of a language forms its type system.
static typing environments
在形式化type rules之前还需要引入另一个不会显式出现在语法中的基本概念——static typing environments：其在处理program fragments的过程中记录free variable的type。一般和编译器在处理typechecking趟时其符号表的内容相对应。
The type rules are always formulated with respect to a static environment for the fragment being typechecked.
比如一个has-type关系M:A，但是这个关系下type A和term M相关的free variable的信息在static environment 𝚪里面的。故这个关系全称应该是𝚪 ⊢ M:A，意思是在静态环境𝚪下，M有A类型。
semantics
形式化程序语言的最后一步就是将其语义定义为一种terms和results之间的relation。该relation的形式很大程度上取决于所采用的语义学风格。语言的语义和type system是相互影响的——term的type和其results应该一样或正相关，这是soundness theorem的本质。
the types of a term and of itsresult should be the same (or appropriately related); this is the essence of the soundness theorem.
type system的基本概念对几乎所有编程范式（函数式，命令式，并行）都是适用的。独立的type rules应用于不同的范式时基本不能改变。比如call-by-name和call-by-value的函数的基本语义是一样的。
这章节我们讨论了独立于语义的type system。但是需要肯定的是，type system一定和一门语义以及该语义所带的soundness相关。
The techniques of structrual operational semantics deal uniformly with a large collection of programming paradigms.
Type equivalence
正向前文所说的，大多数nontrivial type system都会定义一种equal type的关系代表type equivalence。这一属性在定义一门编程语言时候异常重要：什么时候两个分别定义的type expression是一致的？比如两个由相似类型连接的不同type names：
type X = Bool.
type Y = Bool.
如果type namesX和Y因为与相似类型关联而匹配，我们称为structural equivalence。如果由于type names不同而无法匹配（并没有参考相关联的类型），我们称为by-name equivalence。
通常情况下大多数语言会使用structural and by-name的混合。Pure structural equivalence可以通过type rules精确定义，然而by-name equivalence更难确定。后续的讨论我们基本讨论structural equivalence，而by-name equivalence可以使用前者很好的进行模拟。
The language of type systems
Type system定义程序语言的type rules——独立于特定的typechecking algorithms。其和formal grammar定义程序语言的syntax但独立于特定的parsing algorithms是同样的道理。
将type system和typechecking algorithms分离更加高效：type system属于语言定义language definitions，而algorithms属于编译器实现。通过type system映射语言的类型信息要比用编译器算法更加简洁。同一套type system在不同编译器上可能会有多种typechecking算法。
Judgements
Type system由一套特殊的形式化方法描述。下面开始讨论：
首先引入一套形式化机制称作judgments: \[
\Gamma \vdash \Im \qquad \text{ℑ is an assertion;the free variables of ℑ are declared in 𝚪}
\] 读作𝚪 entails ℑ(𝚪包含ℑ)。
𝚪是一个static typing environment，比如一个由不同变量及其相应type组成的有序链表，通过∅, x1:A1, ..., xn:An的形式。空环境记作∅，而在𝚪环境中声明的变量集合x1...xn记作dom(𝚪)——𝚪的domain值域。
ℑ是一种断言，其形式随着不同的judgement会变化，但是ℑ中的所有free variables都必须声明在𝚪中。
a term M has a type A with respect to a static typing environment for the free variables of M. 最重要的
judgement是typing judgement，其断言为：对于针对M中所有free variable的静态环境𝚪的来说，term M的类型是A。
- Term: statements, expressions, and other program fragments
\[ \Gamma \vdash M:A \qquad \text{M has type A in 𝚪} \]
比如举例如下： \[
\begin{aligned}
&\emptyset \vdash true:Bool &&\qquad \text{true has type Bool} \\
&\emptyset,x:Nat \vdash x+1:Nat &&\qquad \text{x+1 has type Nat, provided that x has type Nat}\\
\end{aligned}
\] 其他类型的judgement也很常见，比如下面断言为an environment is well-formed: \[
\Gamma \vdash \diamond \qquad \text{𝚪 is well-formed(i.e., it has been properly constructed)}
\]
Type rules
Type rules：在valid judgements的前提下，断言certain judgement有效。一般都以某些本质上有效的judgements作为开始(常见的有：∅⊢◇,表示empty environment is well-formed)。 \[
\begin{aligned}
&\text{ (Rule name)} \quad \quad \text{ (Annotations)} \\
&\frac{\Gamma_{1} \vdash \Im_{1} \quad ... \quad \Gamma_{n} \vdash \Im_{n} \text{ (Annotations)}}{\Gamma \vdash \Im}
\end{aligned}
\qquad \text{ General form of a type rule.}
\] 每一个type rule的格式：在水平线上面的是一系列premise judgements:𝚪i ⊢ ℑi，而在水平线下面的是conclusion judgements: 𝚪⊢ℑ。当所有的premise都满足之后，conclusion一定成立。premise的数量可以为零。而且每一个type rules都有一个名字：根据惯例，名字的第一个单词是由conclusion judgements规定的~比如conclusion是一个value typing judgement的type rules的名字就会叫做Val...。必要的时候，限制rule的一些条件和需要用到的一些缩写都会在typ rule或者premise旁边进行批注。比如一下例子： \[
\begin{aligned}
&\text{ (Val n) (n=0,1,...)} \\
&\frac{ \Gamma \vdash \diamond }{\Gamma \vdash n:Nat}
\end{aligned} \qquad
\begin{aligned}
&\text{ (Val+)} \\
&\frac{\Gamma \vdash M:Nat \qquad \Gamma \vdash N:Nat}{\Gamma \vdash \text{M+N:Nat}}
\end{aligned}
\] 比如第一个type rule表示所有的numeral自然数都是Nat类型。第二个【结合Typing Judgements】type rule表示两个Nat类型的表达式M和N可以构成一个更大的Nat类型的表达式M+N，Moreover, the environment 𝚪 for M and N, which declares the types of any free variable of M and N, carries over to M+N并且静态环境𝚪不仅声明了M和N的所有free variable的类型，更涵盖了M+N的类型。
注释：首先static typing environment记录程序中free variable的类型信息-These are used to record the types of free variables during the processing of program fragments; 其次typing judgements是断言term有类型-It asserts that a term M has a type A with respect to a static typing environment for the free variables of M。
基本的规则表示empty environment是well formed的，不需要前提： \[
\text{(Env ∅)} \\ \frac{}{\emptyset \vdash \diamond}
\]
A collection of type rules is called a (formal) type system. Technically, type system fit into the general framework of formal proof system: collections of rules used to carry out step-by-step deductions.
The deductions carried out in type systems concern the typing of prorgams.
技术上讲，type system满足形式化证明系统formal proof systems的基本框架：一系列的type rules被用来执行一步一步的推理演绎。类型系统推理的过程就是程序中类型的概念。
Type derivations
derivation在type system中是以judgements tree的形式，上面是叶子，最后是根——每一个judgement都可以从其上面的叶子部分根据一定规则推导得到。type system最基本的要求就是看其derivation是否是正确构建的。
type system中，能正确应用type rules推导出来的一定是valid judgement。比如下面： $$
\[\begin{aligned}
\dfrac{\dfrac{\dfrac{}{\emptyset \vdash \diamond} \text{by(Env ∅)}}{\emptyset \vdash 1:Nat} \text{by(Val n)} \quad \dfrac{\dfrac{}{\emptyset \vdash \diamond} \text{by(Env ∅)}}{\emptyset \vdash 2:Nat} \text{by(Val n)}}{\emptyset \vdash 1+2:Nat} \text{by(Val +)}
\end{aligned}\]
$$ 根据前面给出的规则，我们可以构造出新的derivation即∅⊢1+2:Nat是valid judgement。其中每一步推导用到的规则都标记在右边。
Well typing and type inference
给定一个type system，如果存在一个类型A使得𝚪⊢M:A是有效的——那么对于环境𝚪来说M is well typed的，即term M被赋予某个类型。
The discovery of a derivation(and hence of a type) for a term is called the type inference.
比如在一个简单的type system中，其有rules(Env ∅),(Val n),(Val +)，那么根据前面的推导，在空环境empty environment下的term 1+2可以被推导出Nat类型。假设我们给该类型系统加入premise 𝚪⊢◇和conclusion 𝚪⊢true:Booll，那么我们将无法对term true+1推导出任何类型，这是因为没有一个将natural和boolean类型相加的rule。因为无法推导出1+true的derivations，我们就说1+true是not typeable的，或者说其发生了typing error。我们继续给上述类型系统加入premise 𝚪⊢M:Nat和conclusion 𝚪⊢N:Bool和conclusion 𝚪⊢M+N:Nat（通过将true解释为整数1）。那么term 1+true将会被推导出一个Nat类型。
可以看出，type inference非常依赖type system。一个类型推导算法可以很简单，也可以很难或者压根不可能实现。虽然类型系统通常是抽象表达设计，但是其实用性则完全取决于类型推导算法的可用性。
explicitly typed languages比如pascal的类型推导相对容易简单，而implicitly typed languages比如ML的类型推导相对更困难一些。类型推导的基本思路很清晰易懂，但是真正实际中的实现却相当复杂并且还在研究中。
Type inference problem becomes particularly hard in the presence of polymorphism.
对于explicitly typed languages比如Ada, CLU, ML等的polymorphic features的type inference在实践中得到了解决——是通过纯算法问题，而不是在引入相关type system的基础上解决的。而往往最纯粹，最普遍的针对多态的类型推导问题都是在𝛌演算中讨论的。 然而该问题的结局却依赖于不切实际的冗长的一些typing annotations。为了让该多态方案更加实际化一点，需要省略一些类型信息。这个领域依然是目前学术界的研究重点。
Type soundness
最后需要注意的是，type system不是一系列任意的type rules的堆积。well-typing在语义层面对应着good behavior。通常通过证明type soundness theorem来检查类型系统内部的一致性——因此类型系统需要语义作为基础。对于denotational semantics来说如果∅⊢M:A是有效的，则〖M〗∊〖A〗(即M的值属于类型A所表示的集合)，对于operational semantics来说如果∅⊢M:A成立，并且M推导出M'，则∅⊢M':A成立。对于两个例子来说，type soundness theorem断言well-typed的程序不会在计算过程中出现execution errors。
First-order Type Systems
在大多数过程间语言中实现的type system称为first order。核心就是包括高阶函数higher order functions。最精简的first-order type system可以由untyped 𝛌-calculus表示，形式为𝛌x.M即有参数x和返回值M的匿名函数。
first-order typed 𝛌-calculus被称为F1。它和untyped 𝛌-calculus不同的地方在于对𝛌-abstractions加上了类型信息——𝛌x:A.M其中x是参数，A是参数类型，而M是函数体。将𝛌x.M转化为𝛌x:A.M是将非类型语言进阶为类型语言的关键步骤：bound variables获取到了类型信息。因为F1是建立在函数基础上的，所以引入A⟶B带有参数类型A和返回值类型B的函数类型。介绍构建函数类型所需的基本类型：引入Basic表示该类型集合，引入K∊Basic表示集合中的任何一个该类型。
Syntax of F1
A,B ::= types
K K∊Basic basic types
A⟶B function types
M,N ::= terms
x variable
𝛌x:A.M function
M N application
F1的语法如上图所示。这里有必要简单说明一下typed language的语法。对于untyped language来说context-free syntax就可以完整描述整个语言。而对于typed language来说却不够；typed language不仅仅需要type system来完善程序语言的legality，还需要context-free syntax来表示定义free/bound variable概念——即定义程序语言的scoping rules。在作用域的基础上，那些只有bound variable不同的term会被称为是语法上相同的syntactically identical比如𝛌x:K.x和𝛌y:K.y。
Basic of F1
F1需要三个judgements如下：
| 𝚪⊢◇ | 𝚪 is a well-formed environment |
|---|---|
| 𝚪⊢A | A is a well-formed type in 𝚪 |
| 𝚪⊢M:A | M is a well-formed term of type A in 𝚪 |
其中𝚪⊢A有点冗余，因为所有语法上正确的类型A在任何环境𝚪下都是well-formed的。而在second-order系统中，类型的well-formed就不单单取决于语法了，这时候𝚪⊢A就很重要了。证明这些judgement的有效性的type rules在下面表格中。 \[
\begin{aligned}
&\text{(Env ∅)} \qquad &&\text{(Env x)} \\
&\frac{}{\emptyset \vdash \diamond} \qquad &&\frac{\Gamma \vdash A \quad x\notin dom(\Gamma)}{\Gamma,x:A\vdash \diamond} \\ \\
&\text{(Type Const)} &&\text{(Type Arrow)} \\
&\frac{\Gamma \vdash \diamond \quad K\in Basic}{\Gamma \vdash K} &&\frac{\Gamma \vdash A \quad \Gamma \vdash B}{\Gamma \vdash A\to B} \\ \\
&\text{(Val x)} &&\text{(Val fun)} &&&\text{(Val Appl)} \\
&\frac{\Gamma^{'},x:A,\Gamma^{''}\vdash \diamond}{\Gamma^{'},x:A,\Gamma^{''}\vdash x:A} &&\frac{\Gamma, x:A\vdash M:B}{\Gamma \vdash \lambda x:A.M:A\to B} &&&\frac{\Gamma \vdash M:A\to B \quad \Gamma \vdash N:A}{\Gamma \vdash MN:B}
\end{aligned}
\] 其中规则Env ∅是唯一不需要前提的：空环境empty environment是有效的环境。规则Env x用来将环境𝚪扩展到范围更大的有效环境𝚪,x:A——前提是A在𝚪中是一个有效的类型。注意到对前提𝚪⊢A应用归纳原则就需要𝚪是合法的。也就是说必须由𝚪⊢◇推导出𝚪⊢A。另一个前提是变量x不能在环境𝚪中被使用must not be defined.。我们应该明确在环境中的所有不同变量，比如当ValFun规则中的前提𝚪,x:A⊢M:B被推导时（出现在水平线下面），x就不能出现在dom(𝚪)中。
规则Type Const和Type Arrorw用来构建类型。规则Val x使用非正式的𝚪',x:A,𝚪''表示x:A在环境中的任意地方出现。规则Val Fun对函数𝛌x:A.M赋值了A⟶B类型，前提是首先参数有A类型之后，函数体被赋予了B类型。要注意该规则中environment是如何改变长度的。Val Appl规则将参数传给函数求值。下面展示了F1所有的derivation：
Expansion of F1
现在既然了解过了简单的first-order type system，我们可以通过丰富其内容来将其打造成为一个现实语言的类型系统。我们要为每一个新添加的类型构造添加一组rules。我们首先引入一些基础类型：Unit Type其值就是常数constant unit；Bool Type其值就是true or false；Nat Type其值是自然数。
Unit Type
Unit Type经常用来填充一些空参数和结果比如某些语言中的Void/Null。该类型没有操作，所以我们只需要一条规则陈述Unit是合法的类型，值unit是类型Unit的合法值即可。 \[
\begin{aligned}
&\text{(Type Unit)} \quad &&\text{(Val Unit)} \\
&\frac{\Gamma \vdash \diamond}{\Gamma \vdash Unit} \quad && \frac{\Gamma \vdash \diamond}{\Gamma \vdash unit:Unit}
\end{aligned}
\]
Bool Type
Type Bool也有相似结构的规则，不同的是booleans有一个实际操作——condition。在规则Val Cond中，其两个分支都必须有相同的类型，这是因为这两个都有可能成为结果所以需要保持一致。$$ \[\begin{aligned} &\text{(Type Bool)} &&\text{(Val True)} \\ &\frac{\Gamma \vdash \diamond}{\Gamma \vdash Bool} \quad && \frac{\Gamma \vdash \diamond}{\Gamma \vdash true:Bool} \quad \\\\ &\text{(Val False)} &&\text{(Val Cond)} \\ &\frac{\Gamma \vdash \diamond}{\Gamma \vdash false:Bool} && \frac{\Gamma \vdash M:Bool \quad \Gamma \vdash N_1:A \quad \Gamma \vdash N_2:A}{\Gamma \vdash (if_A \text{M then} N_1 \text{else} N_2):A} \end{aligned}\]
$$ 规则Val Cond引出了一个在typechecking的时候需要用到的类型信息的问题。当遇到条件语句的时候，一般typechecker会分别推断N1和N2的类型，然后在找到一个和前面找到的两个类型兼容的类型A。在一些类型系统中这种推断不是很容易进行，因此为了解决这个问题，我们使用下标类型suubstripted type来表示额外增加的类型信息：ifA就是typechecker的提示：最终类型可能是A，而从N1和N2推断出来的类型信息需要和其做比较。一般情况下我们都会使用下标类型来表示可能会有用的一些类型信息，但是目前比较成熟的typechecker都会自己合成该类型信息，因此其可以省略掉。
Nat Type
自然数的类型Nat Type可以通过0和succ的规则都推导出来。在该类型上的操作通过pred和isZero(测试零值)原语变的可能。 \[
\begin{aligned}
&\text{(Type Nat)} \quad &&\text{(Val Zero)} \quad &&&\text{(Val Succ)} \\
&\frac{\Gamma \vdash \diamond}{\Gamma \vdash Nat} && \frac{\Gamma \vdash \diamond}{\Gamma \vdash 0:Nat} &&&\frac{\Gamma \vdash M:Nat}{\Gamma \vdash succ M:Nat} \\\\
&\text{(Val Pred)} &&\text{(Val IsZero)} \\
&\frac{\Gamma \vdash M:Nat}{\Gamma \vdash pred M:Nat} &&\frac{\Gamma \vdash M:Nat}{\Gamma \vdash isZero M:Bool}
\end{aligned}
\]
Product Type
既然我们有了一系列基本类型，我们可以考虑一些结构化类型，从product Type开始，一个product Type A1XA2表示两个类型分别是A1和A2的元素组成的值对的类型。这两个元素可以分别被投影为projections first和projections second。或者我们可以使用with语句，将一个pair M分解，并将其两个元素绑定在作用域N下的两个变量v1和v2上。with语句对应着ML语言中的pattern matching和pascal语言中的with；
product Type还可以通过相对应的projections和with被用来构建tuple TypeA1XA2...XAi。 \[
\begin{aligned}
&\text{(Type Product)} \quad &&\text{(Val Pair)} \\
&\frac{\Gamma \vdash A_1 \quad \Gamma \vdash A_2}{\Gamma \vdash A_1 \times A_2} && \frac{\Gamma \vdash M_1:A_1 \quad \Gamma \vdash M_2:A_2}{\Gamma \vdash \langle M_1,M_2 \rangle:A_1 \times A_2} \\\\
&\text{(Val First)} \quad &&\text{(Val Second)} \\
&\frac{\Gamma \vdash M: A_1 \times A_2}{\Gamma \vdash firstM:A_1} &&\frac{\Gamma \vdash M:A_1 \times A_2}{\Gamma \vdash second M:A_2} \\\\
&\text{(Val With)} \\
& \frac{\Gamma \vdash M:A_1 \times A_2 \quad \Gamma ,x_1:A_1,x_2:A_2\vdash N:B}{\Gamma \vdash (with(x_1:A_1,x_2:A_2):=M do N):B}
\end{aligned}
\]
Union Type
Type Union经常被忽视，但其和product Type一样重要。一个union:A1+A2的元素可以被看成是有左标记的A1类型（tagged with a left token），或者是一个有右标记的A2类型。这里的标记可以被isLeft/isRight检测其类型结果分别是asLeft/asRight。如果asLeft被错误的赋给right-tagged的值，那么trapped error就会发生。但是这个错误并不是forbidden error。因为假定asLeft有A1类型的情况都是safe的。规则Val Case表述了一种优雅的可以替换isLeft/isRight/asLeft/asRight的构造方式和其相应的trapped errors。其还消除了union对Bool类型的依赖。case构造根据M的标记执行两个分支中的一个，M的未标记内容分别绑定到N1或N2范围内的x1或x2。 $$
\[\begin{aligned}
&\text{(Type Union)} \\
&\frac{\Gamma \vdash A_1 \quad \Gamma \vdash A_2}{\Gamma \vdash A_1+A_2} \\\\
& \text{(Val inLeft)} &&\text{(Val inRight)} \\
& \frac{\Gamma \vdash M_1:A_1 \quad \Gamma \vdash A_2}{\Gamma \vdash inLeft_{A_{2}}M_1:A_1+A_2} && \frac{\Gamma \vdash A_1 \quad \Gamma \vdash M_2:A_2}{\Gamma \vdash inRight_{A_{1}}M_2:A_1+A_2} \\\\
&\text{(Val isLeft)} &&\text{(Val isRight)} \\
&\frac{\Gamma \vdash M:A_1+A_2}{\Gamma \vdash isLeft M:Bool}
&&\frac{\Gamma \vdash M:A_1+A_2}{\Gamma \vdash isRight M:Bool} \\\\
&\text{(Val asLeft)} &&\text{(Val asRight)} \\
&\frac{\Gamma \vdash M:A_1+A_2}{\Gamma \vdash asLeft M:A_1}
&&\frac{\Gamma \vdash M:A_1+A_2}{\Gamma \vdash asRight M:A_2} \\\\
&\text{(Val Case)} \\
&\frac{\Gamma \vdash M:A_1+A_2 \quad \Gamma,x_1:A_1 \vdash N_1:B \quad \Gamma,x_2:A_2\vdash N_2:B}{\Gamma \vdash (case_B Mofx_1:A_1 thenN_1|x_2:A_2thenN_2):B}
\end{aligned}\]
$$ 在程序表达方面而不是实现方面，注意Bool Type可以被定义为Unit + Unit，在这种情况下case的构造就会简化成为condition构造。Int Type可以被定义为一个正数Nat类型加上一个负数Nat类型。
Record Type
Product Type和Union Type类型可以进一步迭代成为tuple Type和multiple unions Type。但是这两种构造太复杂而且不太常出现在现代语言中。而另一中形式labeld的product and union经常被用到：record Type和Variant Type。 \[
\begin{aligned}
&\text{(Type Record)} (l_i \ distinct) \\
&\frac{\Gamma \vdash A_1 \quad ... \quad \Gamma \vdash A_n}{\Gamma \vdash Record(l_1:A_1,...,l_n:A_N)} \\\\& \text{(Val Record)} (l_i \ distinct) \\&\frac{\Gamma \vdash M_1:A_1 \quad ... \quad \Gamma \vdash M_n:A_n}{\Gamma \vdash record(l_1=M_1,...,l_n=M_n):Record(l_1:A_1,...,l_n:A_n)} \\\\
&text{Val Record Select} \\
&\frac{\Gamma \vdash M:Record(l_1:A_1,...,l_n:A_n) \quad j\in 1...n}{\Gamma \vdash M.l_j:A_j} \\\\
&\text{Val Record With} \\
&\frac{\Gamma \vdash M:Record(l_1:A_1,...,l_n:A_n) \qquad \Gamma,x_1:A_1,...x_n:A_n \vdash N:B}{\Gamma \vdash (with(l_1=x_1:A_1,...,l_n=x_n:A_n):MdoN):B}
\end{aligned}
\] record类型可以通过名称来实现提取元素，基本上就是将多个product类型并起来。其规则都是从语法层面按照其元素各自的类型将其进行重组。一个product类型A1XA2可以被定义为Record类型(first:A1, second:A2)。
Variant Type
Variant Type就是复杂版的Union Type。 \[
\begin{aligned}
&\text{(Type Variant)} (l_i \ distinct) \\
&\frac{\Gamma \vdash A_1 \quad ... \quad \Gamma \vdash A_n}{\Gamma \vdash Variant(l_1:A_1,...,l_n:A_n)} \\\\&\text{(Val Variant)} (l_i \ distinct) \\& \frac{\Gamma \vdash A_1 \quad ... \quad \Gamma \vdash A_n \qquad \Gamma \vdash M_j:A_j \quad j\in1...n}{\Gamma \vdash variant_{l_1:A_1,...,l_n:A_n}(l_j=M_j):Variant(l_1:A_1,...,l_n:A_n)} \\\\
&\text{(Val Variant Is)} \\
&\frac{\Gamma \vdash M:Variant(l_1:A_1,...,l_n:A_n) \qquad j\in1...n}{\Gamma \vdash M as l_j:A_j} \\\\
&\text{(Val Variant As)} \\
&\frac{\Gamma \vdash M:Variant(l_1:A_1,...,l_n:A_n \qquad j\in1...n)}{\Gamma \vdash Misl_j:Bool} \\\\
&\text{Val Variant Case} \\
&\frac{\Gamma \vdash M:Variant(l_1:A_1,...,l_n:A_n) \qquad \Gamma,x_1:A_1\vdash N_1:B \quad ... \quad \Gamma,x_n:A_n \vdash N_n:B}{\Gamma \vdash (case_B M of l_1=x_1:A_1 then N_1 | ...|l_n=x_n:A_nthen N_n):B}
\end{aligned}
\] Union TypeA1+A1可以被定义为Variant(left:A1,right:A2)。另外Enumeration Types比如{red, green, blue}可以被定义为Variant(red:Unit, green:Unit,blue:Unit)。其中Is规则是isLeft/isRight，，而As规则是asLeft/asRight，但是如果直接使用union规则的话就需要case处理多个分支。
Reference Type
Reference Type可以被用来处理命令式语言中的mutable locations的基本类型。Ref(A)的一个元素就是一个包含类型A的可变地址。新地址可以被Val Ref分配，或者被Val Assign规则更新，或者使用Val Deref进行解引用。 \[
\begin{aligned}
&\text{(Type Ref)} &&\text{(Val Ref)} \\
&\frac{\Gamma \vdash A}{\Gamma \vdash RefA} && \frac{\Gamma \vdash M:A}{\Gamma \vdash refM:RefA} \\\\
&\text{(Val Deref)} &&\text{(Val Assign)} \\
&\frac{\Gamma \vdash M:RefA}{\Gamma \vdash derefM:A} &&\frac{\Gamma \vdash M:RefA \qquad \Gamma \vdash N:A}{\Gamma \vdash M:=N:Unit}
\end{aligned}
\] 因为赋值语句的目的是为了产生side effect，所以其值就必须是unit-. Since the main purpose of an assignment is to perform a side effect, its resulting value is chosen to be unit
一些常规的mutable类型也可以从Ref类型中派生出来，比如Mutable record types就是一个包含着Ref类型的record类型。
Array Type
array和array操作使用了一些arithmetic primitives and local let declarations等。比较复杂构造的规则可以通过简单构造的规则推导出来。下面给出arrays的实现过程： \[
\begin{aligned}
Array&(A) \quad \triangleq && \text{Array type} \\
&Nat \times(Nat\to Ref(A)) &&\text{a bound plus a map from indices} \text{less than the bound to refs} \\
array_A&(N,M) \triangleq && \text{Array constructor(for N refs initialized to M)} \\
&let \ cell_0:Ref(A) = \\ &ref(M)and...and\ \\ &cell_{N-1}:Ref(A)=ref(M).\\
&in \langle N,\lambda x:Nat.\ if\ x=0 \\
&\ then \ cell_0\ else\ if\ ...\ else\ \\ &if\ x=N-1\ then\ cell_{N-1}\ \\&else\ error_{Ref_{(A)}}.\rangle \\
bound&(M) \triangleq && \text{Array bound} \\
&first \ M \\
M[N]_A &\triangleq && \text{Array indexing} \\
&if\ N\ <\ first\ M \\
&then\ deref\ ((second\ M)(N)) \\
&else \ error_A\\
M[N]:&=P\ \triangleq &&\text{Array update} \\
&if\ N\ <\ first\ M \\
&then\ ((second\ M)(N)):=P \\
&else\ error_Unit
\end{aligned}
\] 下面给出Array类型的规则： \[
\begin{aligned}
&\text{(Type Array)} \\
&\frac{\Gamma \vdash A}{\Gamma \vdash Array(A)} \\\\
&\text{(Val Array)} &&\text{(Val Array Bound)}\\
&\frac{\Gamma \vdash N:Nat \quad \Gamma \vdash M:A}{\Gamma \vdash array(N,M):Array(A)} &&\frac{\Gamma \vdash M:Array(A)}{\Gamma \vdash bound\ M:Nat} \\\\
&\text{(Val Array Index)} &&\text{(Val Array Update)} \\
&\frac{\Gamma \vdash N:Nat \quad \Gamma \vdash M:Array(A)}{\Gamma \vdash M[N]:A} &&\frac{\Gamma \vdash N:Nat \quad \Gamma \vdash M:Array(A) \quad \Gamma \vdash P:A}{\Gamma \vdash M[N]:=P:Unit}
\end{aligned}
\]
Recursive Type
在大多数编程语言中，类型可以被递归定义。Recursive Types让其他类型的构造变的更加有用，但是一般不会显式定义出来，故其形式化方式非常特殊。
处理递归类型需要对F1基础部分做一些增加，environments需要加入type variables X。这个类型变量的形式是𝛍X.A，代表了对递归表达式X=A(X may occur in A)的一种抽象。fold/unfold操作分别映射递归类型及其同型𝛍X.A/[𝛍X.A/X]A（比如[B/X]A意为将在A中的自由出现的X都替换成为B）。这些操作并没有运行时花销，因此在语法中也经常被忽略，但是其存在使得形式化处理变得更加便捷。 \[
\begin{aligned}
&\text{(Env X)} &&\text{(Type Rec)} \\
&\frac{\Gamma \vdash \diamond \quad X \notin dom(\Gamma)}{\Gamma,X\vdash \diamond} &&\frac{\Gamma,X\vdash A}{\Gamma \vdash \mu X.A} \\\\
&\text{(Val Fold)} &&\text{(Val Unfold)} \\
&\frac{\Gamma \vdash M:\lbrack \mu X.A/X\rbrack A}{\Gamma \vdash fold_{\mu X.A}M:\mu X.A} && \frac{\Gamma \vdash M:\mu X.A}{\Gamma \vdash unfold_{\mu X.A/X}M:\lbrack \mu X.A/X\rbrack A}
\end{aligned}
\]
List Type
递归类型的标准应用就是用来定义list和tree，甚至product和union类型。 \[
\begin{aligned}
&List_A \qquad \triangleq \qquad \mu X.Unit+(A\times X) \\
&nil_A:List_A \triangleq \qquad fold(inLeft\ unit)\\
&cons_A:A\to List_A \to List_A \qquad \triangleq \qquad \lambda hd:A.\lambda tl:List_A.fold(inRight\langle hd.tl\rangle)\\
&listCase_{A,B}:List_A \to B \to (A\times List_A \to B) \to B \triangleq \\
&\lambda l:List_A.\lambda n:B. \lambda c:A \times List_A \to B \\
& case(unfold\ l) of \ unit:\ Unit\ then\ n| p:A\times List_A\ then\ c\ p
\end{aligned}
\] Recursive Type可以和Record Type and Variant Type一起定能够以更加复杂的树结构比如abstract syntax trees。而case/with语句就可以被用来解析这些树结构。
当和函数类型联合使用的时候，递归类型变的更加强大。Via clever encodings, one can show that recursion at the value level is already implicit in recursive types: there is no need to introduce recursion as a separate construct. 而且非k类型计算在typed languages中执行了-More precisely, Table 18 shows how to define, for any type A, a divergent element A of that type, and a fixpoint operator A for that type.
最后，Type equivalence在递归类型中显得更加有难度。
Advanced
First-order Type Systems for Imperative Languages
Imperative languages have a slightly different style of type systems, mostly because they distinguish commands, which do not produce values, from expressions, which do produce values产生side effect?
Second-order Type Systems
Type parameter涵盖泛型，类，接口，模板(C++)等高级主题。
SubTyping
针对面向对象。
Equivalence
复杂情况下重构类型相等。
Type inference
统筹类型推导。
暂时总结
本片论文对类型系统做了全范围的综述，进一步深入还需要一些基础。TODO:)