最近看了一篇文章，TypeScript: Static or Dynamic? The war is over.，
它提到了TypeScript是具有gradual typing的编程语言。
所谓gradual typing，维基百科上是这么解释的，
Gradual typing is a type system in which some variables and expressions may be given types and the correctness of the typing is checked at compile-time (which is static typing) and some expressions may be left untyped and eventual type errors are reported at run-time (which is dynamic typing).
编程语言如果具有gradual typing，
它就融合了static typing和dynamic typing双方的特点，
具有gradual typing的语言，也称其类型系统是hybrid的。
看到这里，我发现自己对dynamic typing的理解还不清晰，
于是就翻开了PFPL，
想把相关的概念重新梳理一下。
1. 静态阶段和动态阶段
大部分程序被编写完之后，直到被运行完，一般会经历如下两个阶段（phase），
static阶段，和dynamic阶段。
在static阶段中，我们会对程序进行语法解析，
然后经过类型检查（type checking），以确保程序是良类型的（良构的 well-formed）。
最后在dynamic phase中，执行这些良类型的程序。
—— P35
2. 静态特性
对程序进行的类型检查，由一些断言（typing judgments）组成，
每一条断言，断定特定规则组成的程序，将具有相应的类型，
这通常被称为语言的静态特性（statics）。
—— P35
3. 动态特性
语言的动态特性（dynamics），描述了程序在执行过程中应该符合的限制条件，
有多种方式描述语言的动态特性。
（1）structural dynamics方法
它定义了一个转换系统（transition system），归纳的定义了程序的逐步执行方式。
（2）contextual dynamics方法
和转换系统类似，只不过转换规则的描述方式有些不同。
（3）equational dynamics方法
它由一些定义了程序等价性（definitionally equivalent）的规则组成。
—— P41
4. PCF的静态特性和动态特性
我们以PCF为例，了解一下语言静态特性和动态特性的描述方式，
（1）静态特性
（2）动态特性
上图定义了闭值（closed value）应当满足的推导规则。
第二个推导规则的前提中，中括号表明对它的参数是立即求值（eager）的，
如果省略中括号，则表示是惰性求值（lazy）。
上图定义了转化（transition）应该满足的推导规则。
—— P167-P168
5. untyped calculus的静态特性和动态特性
再看看untyped calculus，
（1）静态特性
（2）动态特性
与PCF不同的是，这里用了equational dynamics方法进行描述。
—— P185-P186
6. untyped means uni-typed
如果支持递归类型，那么untyped calculus可以看成是，
具有统一类型（uni-typed） calculus的类型化版本。
我们可以定义一个这样的递归类型，
因此，函数的参数和函数本身将具有统一的类型（uni-typed）。
—— P190
7. dynamic typing
下面开始介绍dynamic typing了。
将具有dynamic typed的语言，与static typed的语言对立起来看待，是有问题的。
我们可以换一个角度来看，我们说具有dynamic typed的语言，
是static typed的语言的一种特殊情况（special case）——它只有一个递归类型。
—— P193
8. DPCF的静态特性和动态特性
我们来看DPCF（dynamically Typed PCF）的静态特性和动态特性，
（1）静态特性
我们看到，DPCF的值被划分成了两个类别（classes），一个是，另一个是。
它表明，如果包含自由变量，，
则若这些自由变量是良类型的，就是良类型的。
（2）动态特性
其中涉及到的符号解释如下，
—— P194-196
9. hybrid
一个hybrid的语言，指的是它在类型系统中混合了static typing和dynamic typing，
它为static typing语言增加了一个类型，该类型的值需要满足语言动态特性的要求。
DPCF可以嵌入到一个static typed的语言中，被视为一个hybrid的语言。
只需要在static typed的语言中增加一个类型，
可以说，dynamic typing只是static typing的一种特定用法（a mode of use）。
因此，static typing和dynamic typing并不是对立的，
他们可以和谐共存（coexist harmoniously）。
—— P203
10. HPCF的静态特性和动态特性
我们来看HPCF（hybrid PCF）的静态特性和动态特性，
（1）静态特性 
其中，类型中包含了所有具有动态类型的值。
构造器（constructor），会在值上附加一个类别描述符（classifer），以表明它所属的动态类别（class）。
以上类型断言，保证了表达式具有正确的类型。
（2）动态特性
不同类别的值之间进行转换，会产生运行时错误。
—— P203-P204
11. 动态类型与静态类型
dynamic语言和static语言的一些异同点。
（1）dynamic语言将类别（class）关联到值（value）上，
而static语言将类型（type）关联到变量（variable）/表达式上。
与dynamic语言相关的概念是类别（class），而不是类型（type），
例如，，它们可以视为值的标签（tag）。
（2）dynamic语言在运行时（run-time）进行类别检查（class checking），
而static语言在编译时（compile time）进行类型检查（type checking）。
dynamic语言可以看做一类特殊的static语言——该语言中只有一个递归类型。
—— P208