类型系统
编程语言的类型系统为何如此重要？
类型推到的概念？
类型系统为什么如此重要？
动态语言由于缺乏强大的类型系统，会导致什么样的短板？又有什么手段弥补？
一、类型系统的作用
1.错误检查、安全
参考：Luca Cardelli[6], Types and Programming Language
2.程序验证
Curry-Howard 同构简约版：
|
直觉主义极小逻辑 |
类型系统 |
|
命题变元 |
类型变量 |
|
逻辑联接词 |
类型构造算子 |
|
公式（命题） |
类型 |
|
假设 |
变量 |
|
蕴含引入 |
抽象 |
|
蕴含消除 |
抽象 |
|
证明、构造 |
表达式 |
|
证明检查 |
类型检查 |
Dependent Type 家族： Isabelle/HOL, Coq, Agda…
阅读：面向计算机科学的数理逻辑和Software Foundations
3. 文档化
类型签名包含了约束信息，表达了函数的需求，甚至通过签名就猜到实现的方法。
4 程序效率
动态类型不利于编译优化。
例如: JavaScript中，运算中操作数的类型不会静态限定。在结束或者编译产生的代码动态执行中，类型的判断、转换会提高复杂度。
对于能够静态推到出的操作数，可以完全消除其动态运行时的类型检查，
对于那些可以较高概率预测的类型，在JIT中为之生成一个快速的类型处理路径，可以减少不必要的类型检查。
动态类型的消除和快速路径的简化也为其他传统优化提供了机会：如高效的内存分配、循环级化等
二、动态类型、弱类型语言的弥补措施
1 开发策略
测试，最大化覆盖，最大化自动化。
设计模式：设计模式不只是“弥补语言表达式的不足”，也是为了不滥用它的表达力。
其他工程经验
2 程序分析工具（可能与编译器集成）
开发支持工具：
-
模块的依赖分析
-
类型错误检查，pychecker, pylint;
-
内存泄露检测
-
代码风格检查
-
….
编译优化工具：
-
类型分析。如为了做type guided optimization, Spidermonkey 对javaScript 进行类型推到[1]
-
指向分析，动态类型加大了指向分析的难度，D.Jang[7]开发了一个对JavaScript程序的指向分析，并用来优化JavaScript程序的执行，但是精度有限。
-
…
3 改变现有的Type system
把dynamic typing 和 static typing 的优点相结合？
2006年Indiana大学的Jeremyt提出了gradual typing（作者对gradual typing的介绍[2]） 。此后在dyanamic language中挂起一阵“混搭风”..
PEP 483 [3] 提出给Python3.5加gradual typing支持（
@lastmayday
有一个翻译的版本The Theory of Type Hinting），如
def add(x : int):
return x + 1
相关工作可以追溯到POPL 89上Martin Abadi等人的文章[4]。1991年Robert Cartwright提出的Soft typing[5]对后续的发展有很大影响。
利用可选的类型注解，可以使用静态类型检查；可以利用类型信息做编译优化
参考文献
[1] Type Inference in SpiderMonkey
[3] PEP 483
[4] Dynamic Typing in a static typed language
[5] Soft Typing
[6] Type System
[7] http://cseweb.ucsd.edu/~d1jang
类型系统
简介
类型指的是：一个编程语言中的数值、表达式、函数和模块等属性内容。
类型系统包括如何定义这些不同类型，如何操作这些类型，这些类型如何相互作用等方面内容。
类型系统最主要的作用是检查每个值的类型和这些值的流动规则来减少类型错误的发生。
检查可以是静态的，也可以是动态的，或者两者的结合。类型系统也有其他作用，比如编译器优化等。
类型系统是编程语言的一部分，经常被嵌入到解释器和编译器中。它也被一些静态检查工具所使用。
类型错误产生的原因
计算机的硬件层面是无法区分内存地址、指令码、字符、整数、浮点数的，在硬件层面都是bit。类型化就是赋予这些bit意义，那些事内存中的值，那些是一些变量等等。这样能让编程者在更高层次思考，而不用关心比特和字节。但是每种类型所占用的bit数，和作用都是不同的，如果互相之间赋值移动不当，就会造成类型错误。
类型检查
如果一个语言的编译器引入越多的类型检查的限制，就可以称这个语言的类型检查越强，反之越弱。3 / “hello, world"
强/弱类型语言目前业界没有统一的定义，只能说那种语言更强或者更弱一些。
静态类型检查
静态类型检查是基于编译器来分析源代码本身来确保类型安全，不会出现整型除以字符串的情况。静态类型检查能让很多bug在开发早期就被捕捉到，并且他也能优化运行。因为如果编译器在编译时已经证明程序时类型安全的，就不用在运行时进行动态的类型检查，编译过后的代码会优化，运行更快。
但是对于一个图灵完备的语言，静态检查有时可能偏于保守。
if then else
即使test永远为true,对于很多静态检查的语言也会认为以上代码有问题，因为静态分析很难判断else的部分是否可以拿掉。有些编程技术也是无法通过静态方式检查出来的。比如java中的向下转型（父类对象向下转为具体的子类对象，一种不安全的操作）
有很多语言会同时使用静态检查和动态检查，静态证明可以的，动态确定其他部分。
动态类型检查
动态类型检查是在程序运行时进行的。很多类型安全的语言也都包括一些动态类型检查。动态类型检查可能会导致一些运行时错误，有些语言会从错误中恢复，有些会导致fatal error。
编程语言中，把只有动态类型检查没有静态类型检查的语言称为“动态类型语言”
类型安全和内存安全
将不允许操作和转化违反类型系统规则的语言称为类型安全语言
将不允许访问未分配内存的语言称为内存安全语言。比如一个内存安全语言会检查数组越界问题。