类型系统被采用并被作为类型检查的一种手段，从二十世纪五十年代的FORTRAN语言编译器就已开始。采用类型论（type theory）观点的编程语言类型系统的研究，在软件工程、编程语言设计、高性能编译器和网络安全等方面都有重要应用.

2.类型系统（type system）
2.1定义

类型，通常认为是一组可能的值的集合。比如整型，其可能的值是整数的集合；深究系统一词的内涵具有一定的困难。在我们讨论的编程语言这一领域内，当提到“类型系统”时，一个较合理的解释为：一组基本类型构成的“基本类型集合”；及“基本类型集合”上定义的一系列组合、运算、转换方法。
我们可以得到如下的类型系统的定义：
编程语言的组成部分，它由一组定型规则（typing rule）构成，这组规则用来给各种程序构造（变量、表达式和函数等）指派类型
例1: “若M和N都是long类型的表达式, 则M+N也是long类型的表达式”是非形式描述的定型规则

例2：若函数f的某个形参是long类型，则对应的实参也应是long类型。若对应实参是char、short和int类型，则系统会自动把它们提升为long类型。[1]

关于类型系统的定义亦可参见：

A type system is a collection of rules that assign a property called type to various constructs a computer program consists of, such as variables, expressions, functions or modules.[2]

2.2作用

我们知道计算机存储是以二进制方式进行的，并以连续的八个二进制位为一个基本单元——“字节”。以此来看，计算机存储方式是通用的，存储文字、图像、声音或其他别的媒介都没有内在的本质差异。
而实际情况是，我们在编程语言概念上人为引入一系列的迥异的“基本类型”，如C语言中的int和double类型。某种意义上，int和double本身并没有什么差别，都只不过是若干个字节构成的存储单元而已。
那我们为何要设置“复杂”的类型系统？其实就“存储”概念而言，我们用二进制方式，以字节为单位来实现信息的存储，已经足够。但是我们注意到，计算机或者进一步说，编程语言，其作用主要有二，即存储信息和处理信息。事实证明，研究类型理论（type theory），划分类型系统，将在对信息处理方面带来极大便利。

A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.[3]

The fundamental purpose of a type system is to prevent the occurrence of execution errors during the running of a program.[4]

换句话说，设计类型系统的根本目的是利用类型检查（将在下文中介绍）的方式来保证合法程序运行时侯的行为是良好的。
类型化的编程语言除了有助于进行类型检查，较早的发现错误，还另程序模块可以互相独立地编译，并且可得到更有效的空间安排与访问方式。我们也看到由于不同类型数据运算规则的差异，类型系统的存在也是必要的。

并且，结合类型的实际意义，可知，“类型理论解决了使程序具有意义的基本问题，同时引发了一个问题，即一个有意义的程序没有相应的类型与之对应，这也导致了对更加丰富的类型系统的需求。” [5]

2.3相关概念

我们先引入一些下文论述中会出现的概念
trapped errors导致程序终止执行的错误，如除0，Java中数组越界访问
untrapped errors 出错后继续执行，但可能出现任意行为。如C里的缓冲区溢出、Jump到错误地址
Forbidden Behaviors 语言设计时，可以定义一组forbidden behaviors. 它必须包括所有untrapped errors, 但可能包含trapped errors.
Well/ill behaved: 如果程序执行不可能出现forbidden behaviors, 则为well behaved，否则为ill behaved。
了解了以上概念，我们就可以对编程语言进行区分。
1 一种语言的所有程序都是well behaved——即不可能出现forbidden behaviors，则该语言为强类型（strongly typed）。否则为弱类型（weakly typed），比如C语言的缓冲区溢出，属于trapped errors，即属于forbidden behaviors。
2静态类型（statically typed）: 在编译时拒绝ill behaved的程序。
动态类型（dynamiclly typed）: 在运行时拒绝ill behaviors, 
3.如果类型是语言语法的一部分，则是显式类型（explicitly typed）；如果类型通过编译时推导，是隐式类型（implicity typed）, 比如ML和Haskell4.

由此我们可以对常见的编程语言进行分类，分类如下

无类型： 汇编
弱类型、静态类型 ： C/C++
弱类型、动态类型检查： Perl/PHP
强类型、静态类型检查 ：Java/C#
强类型、动态类型检查 ：Python, Scheme
静态显式类型 ：Java/C
静态隐式类型 ：Ocaml, Haskell
4.类型系统的形式化

类型表达式，如：
int, intint, pointer(int)
定型规则，如：

x:int	-x+1:int
其中	-左侧的被称为定型环境 定型断言：

 |– M : int  |– N : int
 |– M + N : int
其中形如

a < b b < c
a < c
的式子我们称之为推理规则。
根据个人理解，定型断言可以看作建立在定型规则之上的一种推理规则。

3.类型检查（Type checking）
编译器对程序进行的检查包括语法检查、类型名变量名及函数名等先声明后引用的检查、类型检查以及其它检查。
我们在此讨论的为类型检查，其实现依赖类型系统。如，若a是long类型的数组，m是long类型，则编译器会发现m + “123”和a + 3.5都有类型错误。
关于类型系统，此处借用来自Wikipedia的定义如下[6]：

The process of verifying and enforcing the constraints of types—type checking—may occur either at compile-time (a static check) or at run-time.

其中提到的两种检查方式为：
Static type checking is the process of verifying the type safety of a program based on analysis of a program’s text (source code).
具体而言，Static type checking不运行被测程序本身，仅通过分析或检查源代码的语法、结构、过程、接口等来检查程序的正确性。静态方法通过程序静态特性的分析，找出欠缺和可疑之处，例如不匹配的参数、不适当的循环嵌套和分支嵌套、不允许的递归、未使用过的变量、空指针的引用和可疑的计算等
Dynamic type checking is the process of verifying the type safety of a program at runtime.
大部分类型安全（type-safe）的语言包含有一些形式的动态类型检测，即使他们同时具有a static type checker，原因在于，许多有用的动能对于静态检查实行起来非常困难。例如，假设有一个程序定义了两个类型A和B，并B是A的一个子类型。此时如果我们要将一个变量从A类型转换为B类型，即对此变量进行向下类型转换，此操作仅在此变量原来即为B类型时才是合法的。而，变量名指向的地址存储的内容只有在程序运行时才可以确定，因此，动态类型检测在判断此类操作是否安全时是必须的。
由此引申第三种类型——Combining static and dynamic type checking。即存在一些编程语言同时允许以上两种类型的检查。

4.c语言的类型缺陷
C语言为笔者唯一较为熟悉的语言，故以此为例。
C语言具有较为完备的静态类型系统，类型可以通过组合产生新的类型 。C的类型包括基本类型和构造类型两种（指针和函数可以看作构造类型）。但是C语言在类型系统上存在着一些不可忽视的缺陷。根据上文中我们介绍类型系统的时候给出的定义， C语言是一种弱类型语言，这会导致在编译过程中的检查是有一定缺陷的，也就有可能会导致程序运行时的安全问题。其中比较常见的不安全运算就是指针运算和类型强制转换。
我们在此处再次举出上课时用到的例子[7]：

typedef struct{int m;float a[];} record;
record p={2,{1.0,2.0}},q={3,{1.0,2.0,3.0}};
int main(){
p=q;
printf(“%d %f %f %f\n”,p.n,p.a[0],p.a[1],p.a[2]);
printf(“%d %f %f %f\n”,q.n,q.a[0],q.a[1],q.a[2]);
return 0；
}
对于这样一段程序，经GCC: (Ubuntu/Linaro 4.6.3-1 ubuntu5)4.6.3编译后会出现以下结果:
3 1.000000 2.000000 3.000000
3432433534 1.000000 2.000000 3.000000
q.n被破坏的原因在于编译器分配连续的内存来存放结构体p和q的数据，导致p.a[1]和q.n的地址相邻，在执行过p=q之后， p.a[2]占用了q.n的地址，q.n的中存储的值被破坏。
又，下面是一个类型转换的例子
/一个初学C会遇到的一个摄氏度转换的算法
f为输入的温度，c为转化后的温度/

main()
{
float c,f;
scanf(“%f”,&f);
c=5(f-32)/9;
}
//根据优先级问题，先算括号里面的，即f-32，由于f是float型，则f-32也是float型
//5和9都是int型，5(f-32)就是int型与float的乘积，此时的int会自动转换为
//float型
//同理，再除9，最终c为float型。
但是实际中经常会出现的问题是，有些同学会把 c=5*(f-32)/9的公式改写成 

c=5/9*(f-32)
即先用5/9再乘括号里的东西，这样的话输出结果会直接为0，因为5和9均为int型，由于int/int=in，所以5/9=0 ，0乘任何数都为0。这样就导致了错误。
弱类型语言与强类型语言并无法判别优劣。在实际工作中，使用哪种语言按需而定。对类型的弱化很多时候提高了语言的灵活性，在编写简单小应用时，使用弱类型语言可，节省很多代码量，有更高的开发效率。例如，C语言的类型系统存在缺陷，这种缺陷造成了C安全上的漏洞，但我们出于效率上的考虑允许了这种不足，所以C语言至今为仍最流行的语言之一。而对于构建大型项目，使用强类型语言可能会比使用弱类型更加规范可靠。

类型系统(type system)是一门编程语言最核心也是最基础的部分。无论该语言基于何种编程范式，都必须在开天辟地之初首先对类型系统作出明确的定义。这是因为，编程语言虽然五花八门，千奇百怪，但是归根结底，编程语言最终的目标，本质上无非是回答两个问题：

如何表示信息；
如何处理信息。
无论是面向过程的编程语言、面向对象的编程语言、函数式编程语言、并行编程语言或者其他任何千奇百怪的编程语言，其根本性的终极目标，就是回答以上两个问题。各种编程语言之所以差异颇大，其实就是对这两个问题给出的答案不同导致的。
在如何表示信息这一问题上，编程语言通常需要定义一些“基本存储单元”，作为整个语言世界的基本构成要素。这种思想很类似于我们对物理世界的认识——宇宙虽然鬼斧神工，丰富多彩，但是在微观上，整个世界仅仅是由少数寥寥几种基本粒子构成的（物理细节不必深究，这里只是打个比方）。但是奇怪的是，基本粒子就只有几种，为何却能构成地球、水、人、树、风这些看似截然不同的东西呢？答案在于，基本粒子虽然不多，但是自然界确立了一套简单而精妙的组合规则，使得基本粒子能够以许多种不同的方式组合在一起，由于组合方式的不同（结构差异），组合规模的不同（数量差异），导致了最终宏观表现的不同。
与现实物理世界类似，一门编程语言就确立了一个独特的“世界”，这个世界可能丰富多彩，千奇百怪。但是就如我们现实世界一样，繁杂的外表之下，骨子里都是由一些“基本粒子”，按照一定的组合方式构成的。那么究竟有哪些基本粒子，又允许进行何种组合，对编程语言所确立的世界最终的宏观结果影响非常巨大。甚至可以说是根本性的。
有一定编程经验的程序员，往往对类型系统不太关心。他们更感兴趣的是语言的其他特性，例如并行计算能力，编程风格，类库等等。这些特性当然非常重要，就生产环境的应用来说，语言特性甚至是处于次要地位的。类库被许多程序员认为比语言本身更重要。然而，坚实的应用是以对语言深刻的理解为基础的，花费一些时间对语言的本质进行研究，会对深入理解语言背后的设计考虑有很大的帮助。也能让我们避免陷入语言的陷阱，或者陷入与别人的口水战之中。
回到对类型系统的考虑，那么究竟什么是类型系统呢？
一门语言定义了一套基本类型的“集合”，这个集合就作为一个整体被称为类型系统。这一称谓中，涉及到两个关键词——“类型”和“系统”。
什么是“类型”？
计算机存储是以二进制方式进行的，并以连续的八个二进制位为一个基本单元——“字节”。从这一点来看，计算机存储是通用的，存储人类的文字或者存储图像、声音或其他别的媒介都没有内在的本质差异。但是奇怪的是，在编程语言概念上，却总是会引入一系列的大相径庭的“基本类型”。例如，int和double，一个存储整数，一个存储浮点数。如果我们考虑一下，就会发现其实int和double本身并没有什么差别，都只不过是若干个字节构成的存储单元而已。那么对他们进行区分意义何在？其实就“存储”概念而言，我们用二进制方式，以字节为单位来实现信息的存储，已经给出了信息表示的“终极答案”了。但是完成存储，只是整个计算机系统功能的一部分。如果仅仅是把信息存储，而不进行计算，那么计算机就不叫计算机，改叫存储机了。可见，问题的实质在于，我们要存储，更要计算。
int和double都是几个字节构成的，但是其运算规则截然不同，差异巨大。同样的，string和int或double也不相同。我们在string上进行拼接、删减、搜索、替换。但是在int上进行加减乘除。这些计算需求和内部实现上的差异，迫使我们的语言层次上进行明显的区分。
上面举的类型，都是来自C家族语言中的概念。但是我们也知道，在一些语言中，不需要我们对类型进行显式的说明。但是不说明不代表不存在。只不过一个是程序员显式声明，一个是编译器（或解释器）自主推导；一个是把责任推给程序员，一个是把责任推给编译器作者。类型系统总是内在的存在的。永远没有被去除。
什么是“系统”？
坦白讲，这是一个非常模糊的概念。我们会说操作系统、消化系统、生态系统……各种各样的系统，然而对于系统本身是什么，在不同的科学领域有截然不同的定义。通常我们所说的系统中，存在一些基本要素（软件模块、细胞、物种等等），然后存在一定的相互作用关系（函数调用、细胞连接、捕食与被捕食等等），在此基础上实现一定的功能（完成金融计算、排解人体毒素、完成有机物的自然循环等等）。那么我们就把这些基本元素，以及其构成方式，统称为一个系统。
之所以说“系统”是个模糊的概念，原因在于，这一概念本身并非原子概念，一个系统，也可能再分解为一系列的子系统，例如操作系统就可以分为输入输出子系统，绘图子系统等等，人体内的消化系统也能够分解为一系列的子系统。而子系统又可在更小的级别进行分解。系统的划分是相对的，系统的构成也是相对的，因此其本身常常是模糊的。
这么说来，如果要追究系统一词的内涵，会很困难。但是在我们讨论的编程语言这一领域内，当提到“类型系统”时，系统其实就是指：

一组基本类型构成的“基本类型集合”；
“基本类型集合”上定义的一系列组合、运算、转换方法。
这两点合起来，就成为了我们的“类型系统”。只要做到这两点，就已经非常强大了。这其中，“基本类型集合”是一个非常小的有限集合，也就寥寥几个元素，而“组合、运算、转换”等规则，也是一个较小的有限集合。但是通过选择不同的元素进行组合，这两个有限的集合之上，却衍生出了一个无限集合——“类型空间”。
理解这一点非常关键。因为这恰好符合了我们对自然界构成的认识——有限的若干种基本粒子，有限的若干种基本规则，结果却是无限可能性的巨大世界。
这一简单优雅而惊人的世界构成观，贯穿了人类现实世界和计算机编程语言所定义的虚拟世界。或许语言的设计者也没有料想到，但是最终的结果确实是有限的设计导出了无限的可能性。
所以，当认识到这一点之后。就再也不会轻视类型系统，再也不会把类型系统看得简单，自以为十分了解了。而类型系统设计上的细微差异，最终也会导致截然不同的类型空间，导致对信息表达方式的巨大差异。

相信有很多跟我一样的读者都是从CCC系语言如JavaJavaJava,C/CPPC/CPPC/CPP等入门开始学习编程。而对我来讲，对于类型系统的概念仅仅停留在JavaJavaJava的泛型语言之中。由于JavaJavaJava的泛型相对来说较为简单，一度让我以为类型不过是些细枝末节，直到我接触到了ScalaScalaScala，HaskellHaskellHaskell这样的语言，才一点一点对类型系统有了较为清楚的认识，同时也开始学习相关方面的知识。

类型系统简介
首先来看看对于类型系统的定义

AAA typetypetype systemsystemsystem isisis aaa tractabletractabletractable syntacticsyntacticsyntactic methodmethodmethod forforfor provingprovingproving thethethe absenceabsenceabsence ofofof
certaincertaincertain programprogramprogram behaviorsbehaviorsbehaviors bybyby classifyingclassifyingclassifying phrasesphrasesphrases accordingaccordingaccording tototo thethethe kindskindskinds
ofofof valuesvaluesvalues theytheythey compute.compute.compute.

类型系统有以下几个优点

Detecting Errors(错误检查)
Abstraction(抽象)
Documentation(文档化)
Language Safety(语言安全性)
Efficiency(有效性)
Further Applications(更多应用)
数学基础
需要读者有集合，序列，归纳等方面的知识，具体可自行查阅

无类型算术表达式
无类型算术表达式主要为了介绍诸如抽象语法，归纳定义和证明，求值，运行时错误等概念的建模。
首先我们需要定义算术表达式的语言形式。以BNF文法形式表达如下

t ::=            terms:
   true         constant true
   false          constant false
   if t then t else t     conditional
   0           constant zero
   succ t         successor
   pred t         predecessor
   iszero t         zero test

语法
归纳定义
true,false,0⊆T;{true, false, 0} ⊆ T ;true,false,0⊆T;
ift1∈T,thensucct1,predt1,iszerot1⊆T;if t1 ∈ T ,then{succ t1, predt1,iszerot1}⊆T;ift1∈T,thensucct1,predt1,iszerot1⊆T;
ift1∈T,t2∈T,andt3∈T,if t1 ∈ T , t2 ∈ T , and t3 ∈ T ,ift1∈T,t2∈T,andt3∈T, thenthenthen ififif t1t1t1 thenthenthen t2t2t2 elseelseelse t3∈T.t3 ∈ T .t3∈T.
推导规则定义
true∈T false∈T 0∈Ttrue ∈ \text{T false} ∈ \text{T 0} ∈ Ttrue∈T false∈T 0∈T
t1∈Tpred t1∈T\frac{t1 ∈ T} {\text{pred t1} ∈ T}
pred t1∈T
t1∈T
​
t1∈Tiszero t1∈T\frac{t1 ∈ T} {\text{iszero t1} ∈ T}
iszero t1∈T
t1∈T
​
t1∈Tsucc t1∈T\frac{t1 ∈ T} {\text{succ t1} ∈ T}
succ t1∈T
t1∈T
​

t1 ∈ T iszero t1 ∈ T t1 ∈ T t2 ∈ T t3 ∈ Tif t1 then t2 else t3 ∈ T\frac{\text{t1 ∈ T iszero t1 ∈ T t1 ∈ T t2 ∈ T t3 ∈ T}}{\text{if t1 then t2 else t3 ∈ }T}
if t1 then t2 else t3 ∈ T
t1 ∈ T iszero t1 ∈ T t1 ∈ T t2 ∈ T t3 ∈ T
​

具体定义
S0=∅S_0 = \emptysetS
0
​
=∅
Si+1={true,false,0}S_{i+1} =\quad \left{\text{true,false,0}\right}S
i+1
​
={true,false,0}
    ∪{succ t1,pred t1,iszero t1 ∣t1∈Si}\cup\left{\text{succ t1,pred t1,iszero t1 }\mid t1 \in S_i\right}∪{succ t1,pred t1,iszero t1 ∣t1∈S
i
​
}
    ∪{if t1,then t2 else t3 ∣t1,t2,t3∈Si}\cup\left{\text{if t1,then t2 else t3 }\mid t1,t2,t3 \in S_i\right}∪{if t1,then t2 else t3 ∣t1,t2,t3∈S
i
​
}

对项的归纳
常量集合
Unexpected text node: ‘&ThinSpace;‘Unexpected text node: ‘&ThinSpace;‘Consts(true) =true
Consts(false)  = false\text{Consts(false) \qquad\qquad\qquad\ = {false}}Consts(false)  = false
Unexpected text node: ‘&ThinSpace;‘Unexpected text node: ‘&ThinSpace;‘Consts(0)   = 0
Unexpected text node: ‘&ThinSpace;‘Unexpected text node: ‘&ThinSpace;‘Consts(succ t1) = Consts(t1)
Consts(pred t1)     = Consts(t1)\text{Consts(pred t1) \qquad\qquad\ \ \ \ = Consts(t1)}Consts(pred t1)     = Consts(t1)
Consts(iszero t1)   = Consts(t1)\text{Consts(iszero t1) \qquad\qquad\ \ = Consts(t1)}Consts(iszero t1)   = Consts(t1)
Unexpected text node: ‘&ThinSpace;‘Unexpected text node: ‘&ThinSpace;‘Consts(if t1 then t2 else t3) = Consts(t1) ∪ Consts(t2) ∪ Consts(t3)

长度
Unexpected text node: ‘&ThinSpace;‘Unexpected text node: ‘&ThinSpace;‘size(true) =1
size(false)  = 1\text{size(false) \qquad\qquad\qquad\ = 1}size(false)  = 1
Unexpected text node: ‘&ThinSpace;‘Unexpected text node: ‘&ThinSpace;‘size(0)   = 1
Unexpected text node: ‘&ThinSpace;‘Unexpected text node: ‘&ThinSpace;‘size(succ t1) = size(t1) + 1
size(pred t1)     = size(t1) + 1\text{size(pred t1) \qquad\qquad\ \ \ \ = size(t1) + 1}size(pred t1)     = size(t1) + 1
size(iszero t1)   = size(t1) + 1\text{size(iszero t1) \qquad\qquad\ \ = size(t1) + 1}size(iszero t1)   = size(t1) + 1
Unexpected text node: ‘&ThinSpace;‘Unexpected text node: ‘&ThinSpace;‘size(if t1 then t2 else t3) = size(t1) + size(t2) + size(t3) + 1

深度
Unexpected text node: ‘&ThinSpace;‘Unexpected text node: ‘&ThinSpace;‘depth(true) =1
depth(false)  = 1\text{depth(false) \qquad\qquad\qquad\ = 1}depth(false)  = 1
Unexpected text node: ‘&ThinSpace;‘Unexpected text node: ‘&ThinSpace;‘depth(0)   = 1
Unexpected text node: ‘&ThinSpace;‘Unexpected text node: ‘&ThinSpace;‘depth(succ t1) = depth(t1) + 1
depth(pred t1)     = depth(t1) + 1\text{depth(pred t1) \qquad\qquad\ \ \ \ = depth(t1) + 1}depth(pred t1)     = depth(t1) + 1
depth(iszero t1)   = depth(t1) + 1\text{depth(iszero t1) \qquad\qquad\ \ = depth(t1) + 1}depth(iszero t1)   = depth(t1) + 1
Unexpected text node: ‘&ThinSpace;‘Unexpected text node: ‘&ThinSpace;‘depth(if t1 then t2 else t3) = max(depth(t1) , depth(t2) , depth(t3)) + 1

引理
一个项上t中不同常量的个数不大于t的长度size(t)，即∣Consts(t)∣≤size(t)一个项上t中不同常量的个数不大于t的长度size(t)，即|Consts(t)| \leq size(t)一个项上t中不同常量的个数不大于t的长度size(t)，即∣Consts(t)∣≤size(t)

定理(项上归纳原理)
假设P是项上的一个谓词：假设P是项上的一个谓词：假设P是项上的一个谓词：

对深度的归纳：如果对每个项s对深度的归纳：如果对每个项s对深度的归纳：如果对每个项s
假设对所有使得depth(r)<depth(s)的项r有P(r)，我们能证明P(s)假设对所有使得depth(r)<depth(s)的项r有P(r)，我们能证明P(s)假设对所有使得depth(r)<depth(s)的项r有P(r)，我们能证明P(s)
则P(s)对所有的s成立则P(s)对所有的s成立则P(s)对所有的s成立
对长度的归纳：如果对每个项s对长度的归纳：如果对每个项s对长度的归纳：如果对每个项s
假设对所有使得size(r)<size(s)的项r有P(r)，我们能证明P(s)假设对所有使得size(r)<size(s)的项r有P(r)，我们能证明P(s)假设对所有使得size(r)<size(s)的项r有P(r)，我们能证明P(s)
则P(s)对所有的s成立则P(s)对所有的s成立则P(s)对所有的s成立
结构归纳：如果对每个项s结构归纳：如果对每个项s结构归纳：如果对每个项s
假设对所有s的直接子项r有P(r)成立，我们能证明P(s)假设对所有s的直接子项r有P(r)成立，我们能证明P(s)假设对所有s的直接子项r有P(r)成立，我们能证明P(s)
则P(s)对所有的s成立则P(s)对所有的s成立则P(s)对所有的s成立

语义形式
指称语义
操作语义
公理语义
求值
求值规则
if true then t2 else t3→t2(E−IfTrue)\text{if true then }t_2\text{ else }t_3 → t_2 (E-IfTrue)if true then t
 else t
→t
​
(E−IfTrue)
if false then t2 else t3→t3(E−IfFalse)\text{if false then }t_2\text{ else }t_3 → t_3 (E-IfFalse)if false then t
 else t
→t
​
(E−IfFalse)
t1→t′1if t1 then t2 else t3→ if t′1 then t2 else t3(E−IF)\frac{t_1 → t_1'}{\text{if }t_1\text{ then }t_2\text{ else }t_3→\text{ if }t_1'\text{ then } t_2\text{ else }t_3}(E-IF)
if t
 then t
 else t
→ if t
 then t
 else t
t
→t
′
​

​
(E−IF)
一步求值关系
项上满足求值的最小二元关系

多步求值关系
多步求值关系是一步求值关系的自反，传递闭包。

范式
如果没有求值规则可以作用于项t，则该项是范式

受阻(stuck)
如果一个封闭项是一个范式但不是一个值，则称该项受阻

haskell实现
首先定义项。由于需要限制if的第一项类型为布尔型故添加了GADTs扩展

{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}

• term
  data Term a where
  TmFalse :: Term Bool
  TmTrue :: Term Bool
  TmIf :: Term Bool -> Term a -> Term a -> Term a
  TmZero :: Term Int
  TmSucc :: Term Int -> Term Int
  TmPred :: Term Int -> Term Int
  TmIsZero :: Term Int -> Term Bool


• show terms
  instance Show a => Show (Term a) where
  show TmFalse = “false”
  show TmTrue = “true”
  show TmZero = “zero”
  show (TmSucc a) = “succ “ ++ show a
  show (TmPred a) = “pred” ++ show a

然后定义两个方法isnumericval和isVal，分别用来检验当前项是值还是数字

isnumericval :: forall a. Term a -> Bool
isnumericval TmZero = True
isnumericval (TmSucc a) = isnumericval a
isnumericval _ = False

isval :: Term a -> Bool
isval TmTrue = True
isval TmFalse = True
isval t = isnumericval t

然后定义求值方法，穷举所有可能项

eval1 :: Term a -> Term a
eval1 (TmIf TmTrue t2 t3) = t2
eval1 (TmIf TmFalse t2 t3) = t3
eval1 (TmIf t1 t2 t3) =
let t1’ = eval1 t1
in TmIf t1’ t2 t3
eval1 (TmSucc t1) = TmSucc t1’
where
t1’ = eval1 t1
eval1 (TmPred TmZero) = TmZero
eval1 (TmPred (TmSucc nv1))
| isnumericval nv1 = nv1
| otherwise = error “unsupport rules”
eval1 (TmPred t1) = TmPred t1’
where
t1’ = eval1 t1
eval1 (TmIsZero TmZero) = TmTrue
eval1 (TmIsZero (TmSucc nv1))
| isnumericval nv1 = TmFalse
eval1 (TmIsZero t1) = TmIsZero (eval1 t1)
eval1 _ = error “unsupport rules”

可以看到上述求值代码有较多冗余，根据多步求值规则重写后如下

eval2 :: Term a -> Term a
eval2 a =
case a of
TmIf t1 t2 t3 ->
case eval2 t1 of
TmTrue -> eval2 t2
TmFalse -> eval2 t3
TmZero -> TmZero
TmSucc a -> TmSucc (eval2 a)
TmTrue -> TmTrue
TmFalse -> TmFalse
TmPred a ->
case a of
TmSucc b -> b
TmZero -> TmZero
_ -> error “unsupport rules”

上述实现可以看到，对于受阻项的处理都为打印错误信息。另外一种处理方式则是定义一个名为wrong的项，用来表示受阻项，有兴趣的可自行尝试。

当然，无类型的算术表达式十分简单。接下来就将进入λ\lambdaλ演算的世界…

无类型λ\lambdaλ演算
基础
变量与元变量(Variables and Metavariables)
首先看一个式子 λ\lambdaλx.λ\lambdaλy.xy有形式λ\lambdaλz.s
其中z,s被称为元变量，x,y被称为对象语言变量

作用域(Scope)
在λ\lambdaλx.t中，x的作用域就为t。而在λ\lambdaλy.xy或者xy中，x就是自由变量。不含自由变量的项成为封闭项，也称为组合子。最简单的组合子是恒等函数：
id=λx.xid = \lambda x.x
id=λx.x

操作语义
β\betaβ规约
(λx.t12)t2→[x→t2]t12(\lambda x.t_{12}) t_2 \rightarrow[x \rightarrow t_2]t_{12}
(λx.t
12
​
)t
2
​
→[x→t
2
​
]t
12
​

其中[x→t2]t12[x \rightarrow t_2]t_{12}[x→t
2
​
]t
12
​
表示由t2t_2t
2
​
代换在t12t_{12}t
12
​
中所有自由出现的xxx得到的项。例如
(λx.x(λx.x))(u r)(\lambda x.x(\lambda x.x))(\text{u r})
(λx.x(λx.x))(u r)

规约后可得到结果
u r (λx.x)\text{u r }(\lambda x.x)
u r (λx.x)

求值策略
考虑项
(λx.x(λx.x))(λz.(λx.x)z)(\lambda x.x(\lambda x.x))(\lambda z.(\lambda x.x)z)
(λx.x(λx.x))(λz.(λx.x)z)

可记作
id(id(λz.id z))id(id(\lambda z.id\text{ z}))
id(id(λz.id z))

这个项包含三个约式：
id(id(λz.id z))‾‾‾‾‾‾‾‾‾‾‾‾‾\underline{id(id(\lambda z.id\text{ z}))}
id(id(λz.id z))
​

id(id(λz.id z))‾‾‾‾‾‾‾‾‾‾‾id\underline{(id(\lambda z.id\text{ z}))}
id
(id(λz.id z))
​

id(id(λz.id z))‾‾‾‾‾id(id(\lambda z.\underline{id\text{ z}))}
id(id(λz.
id z))
​

β\betaβ规约
id(id(λz.id z))‾‾‾‾‾\quad id(id(\lambda z.\underline{id\text{ z}))}id(id(λz.
id z))
​

→id(id(λz.z))‾‾‾‾‾‾‾‾\rightarrow id\underline{(id(\lambda z.z))}→id
(id(λz.z))
​

→id(λz.z)‾‾‾‾‾‾‾\rightarrow \underline{id(\lambda z.z)}→
id(λz.z)
​

→λz.z\rightarrow \lambda z.z→λz.z
正则序
id(id(λz.id z))‾‾‾‾‾‾‾‾‾‾‾‾‾\quad \underline{id(id(\lambda z.id\text{ z}))}
id(id(λz.id z))
​

→id(λz.id z)‾‾‾‾‾‾‾‾‾\rightarrow \underline{id(\lambda z.id\text{ z})}→
id(λz.id z)
​

→λz.id z‾‾‾‾\rightarrow \lambda z.\underline{\text{id z}}→λz.
id z
​

→λz.z\rightarrow \lambda z.z→λz.z
按名调用
id(id(λz.id z))‾‾‾‾‾‾‾‾‾‾‾‾‾\quad \underline{id(id(\lambda z.id\text{ z}))}
id(id(λz.id z))
​

→id(λz.id z)‾‾‾‾‾‾‾‾‾\rightarrow \underline{id(\lambda z.id\text{ z})}→
id(λz.id z)
​

→λz.id z\rightarrow \lambda z.\text{id z}→λz.id z
按值调用
id(id(λz.id z))‾‾‾‾‾‾‾‾‾‾‾‾‾\quad \underline{id(id(\lambda z.id\text{ z}))}
id(id(λz.id z))
​

→id(λz.id z)‾‾‾‾‾‾‾‾‾\rightarrow \underline{id(\lambda z.id\text{ z})}→
id(λz.id z)
​

→λz.id z\rightarrow \lambda z.\text{id z}→λz.id z
λ演算中的程序设计\lambda 演算中的程序设计λ演算中的程序设计
多参数
λ(x y).s→λx.λy.s\lambda \text{(x y)}.s \rightarrow \lambda x.\lambda y.s
λ(x y).s→λx.λy.s

Church布尔式
tru=λt.λf.ttru = \lambda t.\lambda f.t
tru=λt.λf.t
fls=λt.λf.ffls= \lambda t.\lambda f.f
fls=λt.λf.f

条件式
if=λl.λm.λn.l m nif = \lambda l.\lambda m.\lambda n.\text{l m n}
if=λl.λm.λn.l m n

逻辑式
and=λb.λc.b c flsand = \lambda b.\lambda c.\text{b c fls}
and=λb.λc.b c fls
and=λb.λc.b c truand = \lambda b.\lambda c.\text{b c tru}
and=λb.λc.b c tru
and=λb.if b fls truand = \lambda b.\text{if b fls tru}
and=λb.if b fls tru

序对
pair=λf.λs.λb.b f spair = \lambda f.\lambda s.\lambda b.\text{b f s}
pair=λf.λs.λb.b f s
fst=λp.p trufst = \lambda p.\text{p tru}
fst=λp.p tru
snd=λp.p flssnd= \lambda p.\text{p fls}
snd=λp.p fls

数值
c0=λs.λz.zc_0 = \lambda s.\lambda z.z
c
0
​
=λs.λz.z
c1=λs.λz.s zc_1 = \lambda s.\lambda z.\text{s z}
c
1
​
=λs.λz.s z
c2=λs.λz.s (s z)c_2 = \lambda s.\lambda z.\text{s (s z)}
c
2
​
=λs.λz.s (s z)
etc.etc.
etc.

后继
succ=λn.λs.λz.s (n s z)succ = \lambda n.\lambda s.\lambda z.\text{s (n s z)}
succ=λn.λs.λz.s (n s z)

加法
plus=λm.λn.λs.λz. m s (n s z)plus=\lambda m. \lambda n.\lambda s.\lambda z.\text{ m s (n s z)}
plus=λm.λn.λs.λz. m s (n s z)

乘法
times=λm.λn. m (plus n) c0times=\lambda m. \lambda n.\text{ m (plus n) }c_0
times=λm.λn. m (plus n) c
0
​

前驱
zz=pair c0 c0zz = \text{pair }c_0\text{ } c_0
zz=pair c
0
​
 c
0
​

ss=λp. pair (snd p) (plus c1 (snd p))ss=\lambda p.\text{ pair (snd p) (plus }c_1\text{ (snd p))}
ss=λp. pair (snd p) (plus c
1
​
 (snd p))
pred=λm.fst (m ss zz)pred=\lambda m.\text{fst (m ss zz)}
pred=λm.fst (m ss zz)

减法
minus=λm.λn. m (fst (n ss zz))minus=\lambda m.\lambda n.\text{ m (fst (n ss zz))}
minus=λm.λn. m (fst (n ss zz))

递归
ω=(λx.(xx))(λx.(xx))\omega = (\lambda x.\text( x x)) (\lambda x.\text( x x))
ω=(λx.(xx))(λx.(xx))
fix=λf.(λx.f(λy. x x y))(λx.f(λy. x x y))fix = \lambda f.(\lambda x.f(\lambda y.\text{ x x y})) (\lambda x.f(\lambda y.\text{ x x y}))
fix=λf.(λx.f(λy. x x y))(λx.f(λy. x x y))

形式性
定义：一个项t的自由变量集合，记作FV(t)，定义如下：一个项t的自由变量集合，记作FV(t)，定义如下：一个项t的自由变量集合，记作FV(t)，定义如下：
FV(x)={x}FV(x) = {x}
FV(x)={x}
FV(λx.t1)=FV(t1){x}FV(\lambda x.t_1) = FV(t_1) \backslash\text{{x}}
FV(λx.t
1
​
)=FV(t
1
​
){x}
FV(t1 t2)=FV(t1)∪FV(t2)FV(t_1\text{ }t_2)=FV(t_1)\cup FV(t_2)
FV(t
1
​
 t
2
​
)=FV(t
1
​
)∪FV(t
2
​
)

代换
[x→s]x=s[x \rightarrow s]x = s
[x→s]x=s
[x→s]y=y if y̸ =x[x \rightarrow s]y = y\text{ if y}\not=x
[x→s]y=y if y
̸
​
=x
x→s=λy.[x→s]t1 if y̸ =x and y∉FV(s)x \rightarrow s = \lambda y.[x \rightarrow s]t_1\text{ if y}\not=\text{x and y} \notin FV(s)
x→s=λy.[x→s]t
1
​
 if y
̸
​
=x and y∈
/
​
FV(s)
x→s=([x→s]t1)([x→s]t2)x \rightarrow s=([x \rightarrow s]t_1)([x \rightarrow s]t_2)
x→s=([x→s]t
1
​
)([x→s]t
2
​
)

语法
t ::=     terms:
  x     variable
  λx.t    abstraction
  t t    application
v ::=     values:
  λx.t    abstraction value

求值
t1→t′1t1 t2→t′1 t2 (E-App1)\frac{t_1 \rightarrow t_1'}{t_1\text{ }t_2 \rightarrow t_1' \text{ }t_2} \text{ (E-App1)}
t
1
​
 t
2
​
→t
1
′
​
 t
2
​

t
1
​
→t
1
′
​

​
 (E-App1)
t2→t′2v1 t2→v2 t′2 (E-App2)\frac{t_2 \rightarrow t_2'}{v_1\text{ }t_2 \rightarrow v_2 \text{ }t_2'} \text{ (E-App2)}
v
1
​
 t
2
​
→v
2
​
 t
2
′
​

t
2
​
→t
2
′
​

​
 (E-App2)
(λx.t12)v2→[x→v2]t12 (E-AppABS)(\lambda x.t_{12})v_2 \rightarrow [x \rightarrow v_2]t_{12} \text{ (E-AppABS)}
(λx.t
12
​
)v
2
​
→[x→v
2
​
]t
12
​
 (E-AppABS)

项和上下文
为确定变量的出现该如何表示，我们将变量直接指向它的绑定器。这样可以用自然数代替有名变量来实现。例如
λx.x\lambda x.x
λx.x

可表示为：
λ.0\lambda .0
λ.0

而
λx.λy.x(yx)\lambda x.\lambda y.x(yx)
λx.λy.x(yx)

可表示为：
λ.λ. 1 (0 1)\lambda .\lambda .\text{ 1 (0 1)}
λ.λ. 1 (0 1)

移位
要对用自然数代替有名变量的项进行代换，首先需要一个辅助操作，称为移位用来将项中的自由变量重新索引。一个项在截断参数c(表示从第c个索引开始需要移位)上的d步位移，记为↑dc(t)\uparrow ^d_c(t)↑
c
d
​
(t)。定义如下：
↑⏐⏐⏐⏐⏐⏐⏐dc(k)={kk+difk<cifk≥c\uparrow ^d_c(k) =\begin{cases}k& if\quad k < c\ k + d &if\quad k \ge c\end{cases}
↑
c
d
​
(k)={
k
k+d
​

ifk<c
ifk≥c
​

↑dc(λ.t1)=λ.↑dc+1(t1)\uparrow ^d_c(\lambda .t_1) =\lambda .\uparrow ^d_{c+1}(t_1)
↑
c
d
​
(λ.t
1
​
)=λ.↑
c+1
d
​
(t
​
)
↑dc(t1t2)=↑dc(t1)↑dc(t2)\uparrow ^d_c(t_1\quad t_2) =\uparrow ^d_c(t_1)\uparrow ^d_c(t_2)
↑
c
d
​
(t
1
​
t
2
​
)=↑
c
d
​
(t
1
​
)↑
c
d
​
(t
2
​
)

一般用↑d(t)\uparrow ^d(t)↑
d
(t)表示↑d0(t)\uparrow ^d_0(t)↑
0
d
​
(t)

代换
[j→s]k={skifk==jelse[j \rightarrow s]k = \begin{cases}s& if \quad k == j\k&else\end{cases}
[j→s]k={
s
k
​

ifk==j
else
​

j→s=λ.[j+1→↑1(s)]t1j \rightarrow s=\lambda .[j+1 \rightarrow \uparrow^1(s)]t_1
j→s=λ.[j+1→↑
(s)]t

j→s=([j→s]t1[j→s]t2)j \rightarrow s=([j \rightarrow s]t_1 \quad [j \rightarrow s] t_2)
j→s=([j→s]t
[j→s]t
​
)

求值
求值规则稍有变化的地方在于，当一个约式的规约消耗掉某个变量x以后，考虑到该变量x不再是上下文的一部分，所以需要重新生成索引。例如：
(λ.1 0 2)(λ.0)→0 (λ.0) 1(not 1 (λ.0) 2)(\lambda .\text{1 0 2})(\lambda .0)\rightarrow \text{0 } (\lambda .0)\text{ 1} \quad (\text{not 1 }(\lambda .0) \text{ 2})
(λ.1 0 2)(λ.0)→0 (λ.0) 1(not 1 (λ.0) 2)

haskell实现
同样首先定义项

data Term = TmVar Int Int
| TmAbs String Term
| TmApp Term Term
deriving (Show)
定义辅助函数

isval :: Term -> Bool
isval (TmAbs _ _) = True
isval _ = False
定义移位

termShift :: Int -> Term -> Term
termShift d = walk 0
where walk :: Int -> Term -> Term
walk c (TmVar x n)
| x >= c = TmVar (x + d) (n + d)
| otherwise = TmVar x (n + d)
walk c (TmAbs x t1) = TmAbs x (walk (c + 1) t1)
walk c (TmApp t1 t2) = TmApp (walk c t1) (walk c t2)
定义代换

termSubst :: Int -> Term -> Term -> Term
termSubst j s = walk 0
where walk :: Int -> Term -> Term
walk c (TmVar x n)
| x == j + c = termShift c s
| otherwise = TmVar x n
walk c (TmAbs x t1) = TmAbs x (walk (c+1) t1)
walk c (TmApp t1 t2) = TmApp (walk c t1) (walk c t2)
termSubsetTop s t = termShift (-1) (termSubst 0 (termShift 1 s) t)
求值函数

eval :: Term -> Maybe Term
eval (TmApp (TmAbs _ t12) v2)
| isval v2 = return $ termSubsetTop v2 t12
eval (TmApp t1 t2)
| isval t1 = liftM2 TmApp (return t1) (eval t2)
| otherwise = liftM2 TmApp (eval t1) (return t2)
eval _ = Nothing
由于暂时未用到上下文环境，故并未给出定义。

安全，有了类型系统以后就可以实现类型安全，这时候程序就变成了一个严格的数学证明过程，编译器可以机械地验证程序某种程度的正确性，从而杜绝很多错误的发生。
正面例子：Haskell、Rust
反面例子：C，动态语言

抽象能力，在安全的前提下，一个强大的类型系统的标准是抽象能力，能将程序中的很多东西纳入安全的类型系统中进行抽象，这在安全性的前提下又不损耗灵活性，甚至性能也能很优化。动态语言的抽象能力可以很强，但安全性和性能就不行了。
泛型、高阶函数（闭包）、类型类、Monad、Lifetime（Rust） 属于这一块。

工程能力，一个强类型的编程语言比动态类型的语言更适合大规模软件的构建，哪怕不存在性能问题，但是同样取决于前两点。
对于编译器来说能清楚程序的意图，对于人来说也是如此 。一个函数或者类似的东西，说白了就是一个映射关系，Python 中这些映射关系都是没有很明显的约束，要靠约定和默契才能维持，对大型软件来说这是不行的。一个优秀的强类型的程序，很多函数都不需要文档，光看函数申明就可以了。而在安全的前提下的抽象，也是不容易引发灾难的。