理解程序设计语言的类型系统(1)

一、类型系统的作用

近来的新型语言，像Scala，Ceylon，TypeScript，Swift，都有强大的类型系统作为特色和卖点。程序设计语言里的类型，最初的作用是帮助编译器确定某个值要分配多少的内存。例如在Java中，char是16位的，int是32位的，double是64位的。
但是后来，随着程序越来越复杂，如何保证程序的正确性是个需要严肃面对的问题。于是出现了许多测试方法，包括测试驱动开发。
然而，从另一个视角，编译器的类型系统也能帮助软件工程师保证类型安全和正确性。
先进的类型系统，例如依赖类型（Dependent Type）还可以支持程序员做类型级计算（Type level computing）或类型驱动的开发（Type Driven Development）。

在普通值的计算（ordinary value or Term level computing），一个函数的输入和输出都是某些普通的值。
例如一个比较大小的函数max，输入可以是2个整数，输出是一个整数。而类型级计算的函数，输入和输出都可以是某些类型，这有点类似于一些语言中的类型转换，例如当int与double相加时，Java编译器可以自动地把
int转换为double。但是，这只是给编译器使用的功能。像一些现代语言，Haskell或者Idris，则可以把类型转换和计算的功能，暴露给程序员。Scala语言里就提供了类型函数与类型lambda，虽然其语法比较丑。
类型安全能帮助软件工程师写出更加不容易出错的代码。 Tony Hoare（图灵奖得主，快速排序、Hoare逻辑、CSP发明者，启发了ALGOL和Occam语言 ）在2009年一次演讲上说，空引用是他犯的十亿美金的错误 【推荐大家听下】。

《Seven More Languages in Seven Weeks Languages： That Are Shaping the Future语言塑造未来》
The Billion-Dollar Mistake
If you ’ve spent most of your time in dynamically typed languages or even languages like Java and C with very limited type systems, you might have noticed that nil or null values represent a significant percentage of all bugs. These bugs are so prevalent that Tony Hoare referred to null references as a billion-dollar mistake.

业界认为：类型不仅用来塑造我们的对象，类型级编程也能加快计算，这保证了程序员先看到错误，而不是程序的使用者（客户）。
因为类型级编程是由编译器执行的，这无疑会增加编译时间，所以Scalac会比Javac慢，原因之一是由于Scalac可能会做许多高级的类型检查和验证，这个转变是合理的，即把运行期检查
前移到了编译期，有利于提前在编码时发现并修复缺陷。这对提高代码质量和减少开发成本有重大意义。例如最近电软解决方案的许多产品在搞CSEC安全认证，相当一部分是跟类型系统相关的unchecked告警。还有北
研代码基础质量持续提升工作“双零双减半”目标：网上问题减半；内部问题减半：缺陷去除前移等。
在契约编程中，程序员需要写代码保证前置条件与后置条件等不变式，例如某个集合的clear方法后，输入的集合不为null，且输出的集合元素必须是0。又例如有个Animal类有个eat(Food)方法，有2个子类Cow与Dog,继承Animal。但我们要求牛只能吃草，不能吃肉，怎么办呢？
在Java中，这只能在eat方法里用instanceof运行时判断，如果食物是肉，则在运行时抛出疯牛病异常。然后在单元测试里，写一些测试样例，证明程序是正确的（即遵从了不变式约束）。这在Scala中，可以通过抽象的类型成员来实现，由类型系统来证明，程序是正确的，就像是在做数学定理的证明一样 。

二、类型系统简介

在《编译器设计》第2版第4章4.2节里面，专门简介了类型系统-- 我觉得写得比较好了，就直接摘录整理了。
类型：一种抽象范畴，规定了其所有成员共有的性质。常见的类型包括整数、列表和字符等。

类型系统的目标

1.确保运行时的安全性

设计完善的类型系统有助于编译器检测和避免运行时错误。类型系统应该确保程序具有良性的行为，即在病态程序执行导致运行时错误的操作之前，编译器和运行时系统就可以识别出它们。实际上，类型系统无法捕获所有的病态程序，病态程序的集合是不可计算的。
类型推断：为代码中每个名字和每个表达式确定一种类型的过程。
隐式转换：许多语言规定了规则，允许运算符使用不同类型的值，并要求编译器按需插入类型转换操作。另一种备选方案是要求程序员指定显式转换。
安全性是使用强类型语言的一个重要原因。如果语言的实现能够保证在程序执行之前捕获大多数类型相关的错误，这将简化程序本身的设计和实现。如果一种语言中每个表达式都能够分配一个无歧义的类型，这种语言称为强类型语言。如果每个表达式只能在编译时确定类型，我们称这种语言为静态类型的（statically typed），如果某些表达式只能在运行时确定类型，称这种语言为动态类型的（dynamically typed）。还有另两种语言：无类型语言，如汇编代码和BCPL语言；和弱类型语言，即类型系统较为贫乏的语言。

2.提高表达力

与上下文无关相比，具有良好结构的类型系统请允许语言设计者更精确地规定程序的行为。这种能力使得语言设计者可以加入一些上下文无关语法不可能表示的特性。一个出色的例子就是运算符重载，即赋予运算符上下文相关的语义。
运算符重载：如果运算符的语义是根据其参数类型定的，那么该运算符是被“重载”的。

3.生成更好的代码

设计完善的类型系统为编译器提供了程序中每个表达式的详细信息，通常利用这一信息进行转换可以生成更高效的代码。
从性能角度来看，编译时检查总是更可取。但语言设计方面的考虑才能确定编译时检查是否是不可能。
4.类型检查
为避免运行时类型检查的开销，编译器必须分析程序，为每个名字和表达式分配一种类型。它必须检查这些类型，以确保类型在相应的上下文中的使用是合法的。总而言之，这些活动通常称为类型检查。不过这是个误称，它将类型推断和识别类型相关错误的不同活动放在了同一个名称下。

类型系统的组件

典型现代语言的类型系统有四个主要组件：一组基础类型（或内建类型）、根据现存类型创建新类型的规则、用于确定两种类型是否等价或兼容的方法、用于为每个源语言表达式推断类型的规则。许多语言也包括了根据上下文将一种类型的值隐式转换为另一种类型的规则。

1.基础类型

大多数程序设计语言都提供了基础类型，用于表示下述数据种类中的一些或全部：数字、字符、和布尔值。

2.复合类型和构造类型

虽然程序设计语言的基础类型通常对硬件直接处理提供了足够的抽象，但它们通常不足以表示程序所需的信息。程序通常都需要处理更复杂的数据结构，如图、树、表、数组、记录、列表和栈。
多态性：可以运行于不同类型参数之上的函数称为多态函数。如果类型集必须显式地规定，该函数使用了非参数化多态性（ad hoc polymorphism），如果函数体并不规定类型，它使用的是参数化多态性（parametric polymorphism）。

3.类型等价性

对任何类型系统来说，都有一个关键组件，即用于判断两种不同类型声明是否等价的机制。
历史上，已经尝试过两种通用的方法。前一种是所谓的名字等价性（name equivalence），该规则断言两个类型等价的充分必要条件是二者同名。该规则从哲学上假定，程序员可以为一个规则选择任何名字，如果程序员选择不同的名字，语言及其实现应该认可这种有意的选择。遗憾的是，随着程序规模、作者数目、不同代码文件数目的增长，维护名字一致性的难度激增。
第二种方法是所谓的结构等价性（structural equivalence），该规则断言两个类型等价的充分且必要条件是二者有相同的结构。该规则从哲学上断言，如果两个对象由同一组字段组成，且字段排列顺序相同，且对应的字段具有等价的类型，则两个对象 类型是可互换的。结构等价性考察了定义了类型本身的那些基本性质。

4.用于推断的规则

一般来说，用于推断类型的规则会对每个运算符规定操作数类型和结果类型之间的映射。
操作数类型和结果类型之间的关系，通常定义为表达式树上的一个递归函数。该函数将运算的结果类型作为其操作数类型类型的一个函数，来进行计算。
类型推断规则可以指出类型错误。
类型系统的分类
检查实现与无检查实现 程序设计语言的实现可以选择执行足够的检查，来检测并阻止类型误用导致的所有运行时错误。（这样做实际上可以消除一些特定于值的错误，如除以零。）我们将这种实现称为强检查的（strongly checked）。与强检查实现相对的是无检查实现，即假定程序本身是良构的。在这两种极端情况之间，还有若干弱检查的（weakly checked）的实现，这些实现只进行部分检查。
编译时活动与运行时活动 强类型语言可以有这样的性质：所有推断和检查都可以在编译时完成。如果语言的实现确实在编译时完成了所有这些工作，则称为静态类型（statically typed）和静态检查的（statically checked）。一些语言包括了某些结构，必须在运行时确定其类型并检查。我们将这些语言称为动态类型（dynamically typed）和动态检查的（dynamically checked）。更容易令人迷惑的是，编译器编写者可以通过动态检查来实现一种强类型的静态类型语言。Java是这种语言的一个例子，它本身可以静态类型和静态检查的，只是其执行模型导致编译器无法立即看到所有源代码。这迫使编译器在加载类文件时进行类型推断，并在运行时执行一部分类型检查工作。

5.推断表达式的类型

推断类型的目标是为程序中出现的每个表达式分配一个类型。类型推断的最简单情形是编译器可以为表达式中的每个基本元素分配一个类型，亦即，表达式语法分析树中的每个叶结点都可以分配类型。

6.类型推断的过程间相关问题

表达式的类型推断固有地依赖于形成可执行程序的其他过程。即使在最简单的类型系统中，表达式也会包含函数调用。编译器必须检查每个调用。它必须确保每个实参（actual parameter）的类型兼容于对应的形参（formal parameter）。它还必须确定返回的值的类型，以供进一步推断使用。

本节回顾

类型系统将某些文本字句关联到程序中的每个值，这就是类型，它表示了所有此类型值共有的一组性质。程序设计语言的定义规定了同一类型对象之间的交互，如对某 类型值的合法操作，还规定了不同类型对象之间的交互，如混合类型算术操作的语义。设计完善的类型系统可以增强程序设计语言的表达力，允许安全地利用重载之 类的特性。它还能尽早暴露程序中微妙的错误，以免程序给出错误的结果，或者在运行时出现费解的错误。它可以让编译器避免浪费时间和空间的运行时检查。
类型系统包含一组基本类型、基于现存类型构建新类型的规则、用于判定两个类型等价性的方法以及用于推断程序中每个表达式类型的规则。使用过高级语言编程的人对基本类型、构造类型和类型等价性等观念都应该很熟悉。在编译器的实现中，类型推断扮演了关键的角色。
在第4章5.1节里面，简略地叙述了类型推断中更困难的问题
强 类型、静态检查的语言通过检测大量各类错误的程序，有助于程序员产出有效的程序。这一特性同样可以提高编译器上生成高效代码的能力：即消除（不必要的）运 行时检查，同时揭示出一些特定的位置，在这些位置上编译器可以针对某些结构进行特化处理，以消除处理运行时不可能出现的情况的代码。这些事实部分地解释了 类型系统在现代程序设计语言中不断增长的作用。
类型化规则是语言定义规定的。这些规则的具体细节决定了为各个变量推断类型的难度。这一点，进而又对编译器可用于实现语言的策略有着直接影响。
1. 类型一致的用法和恒定的类型函数
2. 类型一致的用法和未知类型函数
3. 类型的动态改变

【类型系统的主题会是一个系列，敬请期待下一篇^_^】