柯里化的前生今世(十):类型和类型系统

  1. 云栖社区>
  2. 博客>
  3. 正文

柯里化的前生今世(十):类型和类型系统

何幻 2016-10-28 11:55:48 浏览1344

形式化方法

在计算机科学中,尤其在软件工程和硬件工程领域,
形式化方法(Formal method),是一种数学方法,用于软件和硬件系统的描述(specification)、开发(development)和验证(verification)。旨在能像其它工程学科一样,通过用数学进行分析,来提高设计的可靠性(reliability)和健壮性(robustness)。

为了让系统表现的和规范(specification)一致,现代软件工程采用了一系列的形式化方法。其中包括一些强有力的框架,例如,霍尔逻辑(Hoare logic),Algebraic specification language(Specification language),模态逻辑(Modal logic),指称语义(Denotational semantics)。它们虽然功能强大,但是对程序员来说门槛较高。

另一方面,还有一些轻量级的技术,可以被植入编译器,连接器或程序分析器中,进行自动校验。从而,那些不熟悉底层理论的程序员也可以使用它们。模型检测(Model checking),运行时验证(Runtime verification)和类型系统(Type system)是常见的轻量级形式化方法。其中类型系统最流行,发展最完善。

历史

在计算机科学中,最早的类型系统用来区别数字的整数和浮点数。
在20世纪五六十年代,这种分类扩展到了结构化的数据和高阶函数中。
70年代,研究者们引入了几个更为丰富的概念,例如,参数化类型,抽象数据类型,模块系统,子类型等等,类型系统作为一个独立的领域形成了。

计算机科学家们也开始意识到,程序语言中的类型与直觉主义逻辑中的命题,之间的联系,称为Curry–Howard correspondence,开始了两方面的交叉研究。后经范畴论(category theory)的探索,得到了三方面的同构关系,Curry-Howard-Lambek correspondence。

类型系统

类型系统使用了证明论(Proof theory)方法,通过给程序中的值指定不同的种类,来证明程序的某些行为不会发生。

使用类型系统的初衷,是想保证程序不会出现运行时错误(Execution error),然而,
一方面,对于什么是一个『错误』,还需要详细说明,
另一方面,程序是否会出现运行时错误,是不可判定的。
(可判定性:Decidability)

因此,这里的『错误』应该是所有运行时错误的一个子集,
那些类型系统被证明为具有可靠性(Soundness)的程序设计语言,
类型合法的程序才能保证不会出现给定的『错误』。

1. 运行时错误

当程序被要求做一些未定义的事情时,就会产生Execution error,导致程序崩溃(crash)。Execution error会在运行时表现出来,因此也称为运行时错误(run-time error)。

运行时错误,通常包括以下两种。

有一种运行时错误不会立即表现出来,比如数组越界,或者程序跳转到错误的地址。它们不会被立即注意到,但是过了一会就会产生一个出乎意料的结果,我们将这种错误称为『未捕获的错误』(untrapped errors)。

而另外一种运行时错误,比如除零,或者访问非法的内存地址。程序会马上出错并停止执行,这种错误称为『被捕获的错误』(trapped errors)。

2. 安全性

如果一块代码不会产生『未捕获的错误』,就称它为安全的(safe)。
如果语言中的所有程序都是安全的,就称该语言是安全的。
因此,语言如果具有安全性,就不会发生潜在的运行时错误。

无类型语言和类型化的语言都可以保障安全性。
无类型语言可以使用运行时检测来实现,而类型化的语言通过类型来拒绝那些可能会出现不安全性质的程序,类型化的语言也可能会混用运行时检测和类型校验。

3. 类型化

程序中的变量在程序执行期间,可能会有不同的取值范围,
我们把变量可取值的最大范围称为这个变量的类型(type)。
例如,具有类型Boolean的变量x,在程序执行期间,只能取布尔值。
指定类型之后的程序设计语言,称为类型化的语言(typed language)。

如果一个语言,不限制变量的取值,就称为无类型语言(untyped language),我们既可以说它不具有类型,也可以说它具有一个通用类型,这个类型的取值范围是程序中所有可能的值。

4. 类型标记

类型系统是类型化语言的一个组成部分,它用来计算和跟踪程序中所有表达式的类型,从而判断某段程序是否表现良好(well behaved)。

类型化语言是得益于类型系统,而与代码中是否具有类型标记无关。
如果程序语言的语法中含有类型标记,就称该语言是显式类型化的(explicitly typed),否则就称为隐式类型化的(implicitly typed)。

主流类型化的语言,都是显式类型化的。
但是,ML和Haskell可以省略类型声明,它们的类型系统会自动推断出程序的类型。

5. 什么是『错误』

判断一块代码是否具有运行时错误,这个问题是不可判定的,
即,在不运行这块代码的情况下,不存在一个通用算法回答是或否。

因此,实际操作上,我们需要缩小待排除的运行时错误的范围。
我们指定一个运行时错误的子集,它包含所有的『未捕获的错误』,还包含一部分『被捕获的错误』,我们称这些错误为『被禁止的错误』(forbidden error)。

如图所示:

如果程序不会产生『被禁止的错误』,就说该程序『行为良好』(well behaved),因此『行为良好』的程序一定是安全的。

程序的安全性比『行为良好』更重要,类型系统的主要目标就是保证程序的安全性——在运行时不会出现『未捕获的错误』。
然而,实际操作中,大部分类型系统被设计成保证程序的『行为良好』,从而也能保证程序的安全性。

6. 静态检测和动态检测

为了避免歧义,下文不再使用静态类型和强类型这样的术语,来表示语言的全局特征,而是使用了静态检测(statically check)和强类型检测(strongly check),来表示某个阶段或者这个阶段的性质。

如果某个类型化的语言可以不通过运行,只通过编译时的静态检测(statically check),来保证程序的『行为良好』,这样的语言称为『被静态检测』的语言。

如果某个无类型语言,可以在运行时排除『被禁止的错误』,就称为『被动态检测』的语言。(这里指的是动态检测,而不一定是动态类型检测

语言被动态检测,也并不意味着运行时可以不加检测的执行。
被静态检测的语言,通常也需要一些运行时检测,来保证安全性。
例如,数组越界,通常使用动态检测来确定。

7. 类型系统的强弱

一个类型化的语言,如果所有合法的程序都是『行为良好』的,就称该语言是被『强类型检测』的(strongly checked)。

因此,强类型检测的语言具有以下特征:
a) 不会发生『未捕获的错误』——安全性。
b) 那些指定为『被禁止的错误』的『被捕获的错误』不会发生。
c) 一些『被捕获的错误』可能发生,需要程序员来避免。

相反,如果某些『未捕获的错误』不能被静态检测,就有可能出现不安全的代码,我们就称该语言是被『弱类型检测』的(weakly checked)。

下文

有了这些铺垫以后,我们就可以用Haskell来学习类型系统了,
这是一个不错的体验。

参考

Types and Programming Languages
Type systems: Luca Cardelli