什么是类型安全? - Githubissues

title: 什么是类型安全? date: 2017-03-16 15:30:48 tags:

类型系统
程序语言理论

什么是类型安全？

有时候有些人说，Java是个类型安全的语言，那么这些人到底是在说什么？所有的类型安全的语言是一样的吗？

事实上，一个语言类型安全的定义是取决于语言类型系统的定义。简而言之，类型安全能保证程序的行为是意义明确的（well-defined）。更广泛的来说，我将要讨论的话题就是，一个语言的类型系统是推导程序正确性，安全性的一个有利工具。类型系统也是程序语言理论一个热门的研究领域。

思考下，为什么动态类型的语言，比如，Python，Javascript这些语言没有良好的代码提示工具呢？也为什么没有良好的函数定义跳转工具呢？

其实就是由于类型系统的影响，导致没有工具能非常正确分析程序结构，导致跳转，提示不正确。简单的程序可能可以分析出来，但是一旦程序结构复杂了，就难以作出代码的正确提示。所以为了弥补Javascript的不足，才有了静态类型的TypeScript，这样静态类型的语言在语言编译的时候就可以借助编译器或者静态分析工具分析出大量隐含的错误(警告)，也更利于为其开发良好的代码提示，重构工具，也更利于大型项目的开发维护。好处是不言自明了。

基本的类型安全

类型安全基本可以用一句话总结：有良好的类型系统的语言能保证自身程序不出错。

这句话其实不是我创造的，是来自于Robin Milner他1978年的一篇论文，论文叫《A Theory of Type Polymorphism in Programming》。翻译过来就是，编程中的类型多态理论。

好，下面我们来逐步讲解这句话是什么意思。

1. 程序出错

编程语言是由其语法和语义定义的，语法就是程序该怎么写。语义就是程序的表述意义。

其实对于现实中的语言来讲，很多表达方法都是语法正确，但语义存在问题的。

就拿一个顶级语言学家乔姆斯基(Chomsky)经典的英文例子来说，Colorless green ideals sleep furiously。这句英文语法上是完全正确的，但是句子表述的意义本身毫无意义，无颜色的绿色是什么鬼？

再来一个Ocaml编程语言的例子，1 + "foo" , 根据Ocaml语言的语义这个句子毫无意义，数值和字符串做加法是什么鬼？

还有个C语言的例子：

char buffer[5];
buffer[5] = 'F';

以上代码语法完全正确，但是数组的下标越界了，在C语言规范中，这样的写法是未定义行为(undefined bahavior)。这是毫无意义的，基于该语句所导致的任何后果现象作出讨论都是无意义的，程序可能崩溃，也可能看上去“运行良好”，但是实际上已经错了。无意义的程序就是错误。类型系统就是为了对这样的行为做出约束。

2. 良好的类型系统可以保证程序不出错

在类型安全的语言中，其类型系统能保证程序的正确运行，如果说，一个语言的类型系统能保证程序不出错,我们就可以说这个语言是良好类型的(well-typed)的。一个well-typed的语言肯定是well-defined的语言。 well-defined包含well-typed,well-typed包含于well-defined。

在类型安全的语言中，well-typed的语言是well-defined语言的子集，它们都是语法正确的语言的子集。

all langauge > well defined language > well typed language

什么语言才是类型安全的？

我们来看看几种流行的语言是否是类型安全的。

1. C/C++

非类型安全，C语言的类型系统不对无意义的行为做约束，例子数组越界。而C++可以认为是C语言的超集（为了兼容垃圾C语言这个历史包袱不得不作出的妥协），也没有对数组下标越界作出约束，所以也是非类型安全的。当然还有为了兼容C，C++允许随意的强制类型转换很容易破坏类型系统。所以更加类型安全的类型转换，dynamic_cast, static_cast, const_cast等。

2. C#/Java

可能是类型安全的，因为很难通过观察对一个成熟的语言实现作出断言。例如，早期的Java版本泛型的类型推导是不正确的。当然一种叫Featherweight Java的方言就是类型安全的。至于为什么，可以告诉你，这是理论证明出来的。

有趣的是，满足类型安全的一个要点就是，C语言的语义没有对数组越界作出约束，而C#和Java对于数组越界统统会抛ArrayBoundsException的异常。

3. Python/Ruby

它们是否是类型安全的值得商榷。Python和Ruby往往被人称作动态类型(也被称作鸭子类型)语言，它们在执行中如果发生类型错误，就会抛出异常。就像Java对于数组越界在运行时会抛出异常，Ruby也一样，在运行时如果进行一个整数和字符串类型的加法也会抛异常。这样的行为是被语言的语义所规定约束的，所以它们都有良好的定义(well-defined)。

事实上，正是语言的语义赋予程序以意义。所以就本身而言，这些语言都是类型安全的，这种类型安全依赖于一种"无类型"系统(null type system),因为它能接收任何程序并且不让程序出错稳定运行。因此，是类型安全的。

这个结论看样子有点奇怪。在Java中，如果一个程序, object.method()被视为well-typed。那么类型安全会保证object是一个真正合法的对象，所以对method方法的调用总会成功。如果换做Ruby的话，那么object.method()依赖于Ruby的null type system保证是well-typed，虽然当我们运行Ruby的这段程序（没有任何保证object对象确实定义了一个叫method的方法），这段程序要么成功，要么会抛出异常，它确实会正常运行下去。如果是Java直接在编译时就报错了。

所以简短来说，类型安全不是万能的，类型安全所作出的保证是依赖于语言的语义的，语义隐式定义了语言的错误的行为(wrong behavior)。在Java中，这样调用一个不存在的方法就是错误的行为，在Ruby中，就不是错误的，它仅仅是抛出一个异常。

深入点的探讨

一般来说，类型安全确确实实是有用的，如果没有它，我们就无法保证程序按照我们的意图，并像它们所定义的那样运行下去，这样程序就能做一些非法的事了。

C/C++对未定义行为作出了一定程度的忍让，所以这也让C/C++编写的程序是导致很多漏洞，软件攻击的根源,比如stack smashing,利用栈溢出进行攻击，再比如格式化字符串攻击。这种类型的漏洞和攻击是不可能发生在类型安全的语言编写的软件中的。

上面只是简单对Java和Ruby作出了一定的阐述。下面来对类型系统做一些更深入的探索。不是所有语言的类型系统都一样，有些类型系统能保证的指标，其他类型系统却不能保证。所以，我们在探索一门语言的时候，不要只确认它是否是类型安全的，而是确认这个类型系统满足了哪些指标，哪些指标是你所关心的，哪些不是。废话了这么多，下面开始吧。

1.缩小鸿沟

之前文章提到过，well-defined > well-typed，well-defined的语言不一定是well-typed。所以这两者类型系统之间有什么区别呢？从well defined到well typed的过渡是什么情况？先说结论，这类过渡的语言都是well defined的，但是这类语言的类型系统不会“拒绝”，举个例子，对于大多数类型系统会“拒绝”下面一段程序：

//虽然是javascript的语言的语法，但是不要理解成js语言，这里
//只是为了方便表述思想
function test(p){
 var x;

 if (p) x = 5;
 else x = "hello";
 if (p) return x+5;
 else return strlen(x);
}

这个函数，无论p的值是true，还是false，该函数都会返回一个int类型。但是如果是非well typed语言的类型系统就不会会“拒绝”这段程序，而well typed语言的类型系统会“拒绝”这段程序。因为变量x的类型“同时”是String类型和int类型，用类型推导的理论就是，bool -> int ^ bool -> String，这种表示的是intersection type,而不是union type。intersection type表示的是变量x“同时”是String和int类型，而不是“有时”是String类型，“有时”是int类型。

再举个类似的例子：

function test(param){
    return param;
}

var a = test(1);
var b = test(true);
var c = test("Hello");

以上的函数test类型就是intersection type的，bool -> bool ^ String -> String ^ int -> int 。也就是函数的输出输入可以"同时"是这三种类型。如果是Union Type,那么调用test(1)就会报错，因为test函数类型还有可能是bool -> bool ， String -> String。调用test(true),test("Hello")都会出错，原理一样的，左右不是人。垠神的文章也解释过。

回过头来看第一段程序，根据静态分析工具其语言的类型系统是正确但不完备的。这不完备性也让很多程序员失望。一个补救的措施就是，让其类型系统能够处理，缩小well-defined与well typed的鸿沟。

给一个参考，JavaScript是无类型的语言吗?

一个例子，Java的类型系统在1.5版本的时候引入了泛型的概念，在1.4中，你需要类型转换来告诉java的类型系统来接受程序，1.5就不需要转化了。另一个例子是lambda演算，函数式编程语言的基础，lambda演算其中一个加入类型的版本叫Simply Typed lambda calculus，这个类型系统相对于Milner’s polymorphic type system能接受更少的程序，而Milner's type system又比支持Rank-2 (or higher) polymorphism的类型系统接受更少的程序。

所以设计一个完备，表现力强大，可用的类型系统是程序语言理论的热门领域。

2.强制不变性

一些你所见过的经典编程语言都有类型声明，int，string等等。类型安全可以保证表达式的类型必须与类型所声明的一致。不必限于int类型，一个类型系统可以支持更加广泛丰富的类型，从而表达程序更加有趣的特性。

比如在研究领域一个细化类型(refinement types)有趣的例子，就是利用逻辑公式描述一个类型一组的可能的值。类型{v: int | 0 <= v},用公式0 <= v细化了int类型，它简洁高效的定义了非负整数类型。细化类型允许程序员为数据结构的类型表达数据结构不变性，类型安全正是由于这些不变性保证的。细化类型系统已经有实例了，比如，在Haskell中的Liquid Haskell,F#中的F7。

另一个例子,我们可以用类型系统(通过强制共享数据不变性)，来防止数据竞争(data race)。这个情况下，那么共享变量的类型本质上就是一个锁来保护它的不变性。这样叫Types for safe locking第一次是在Abadi 和Flanagan的文章中第一次被提及。这个特性有Java版本的实现,戳这里。也有C语言版本的实现。

当然还有很多使用有趣类型系统的例子，限制被污染数据的使用，防止私有信息的泄露等等。

3.类型抽象和信息隐藏

许多编程语言都允许数据抽象（也叫信息隐藏）。这些语言提供了一些抽象手段，比如提供类(classes)，模块(modules)，函数(functions)这样的概念。它们可以把内部的结构不暴露给使用者,面向接口编程，接口不变，实现变化。

类型系统在这样的抽象中就扮演至关重要的角色。表述独立(Representation independence)说明了程序的运行只应该依赖其抽象，不应该依赖其实现。之后的John Reynolds在类型和抽象上又做出了开创性的工作，发表于他1983年的一篇paper，用一句简单的话来概括这论文就是，类型结构是维护抽象级别的一个语法工具，也就是说，类型是构建可维护系统的最基础重要(fundamental)的角色。

所以！！！！

为啥Haskell写出来的代码在懂的开发人员面前更好维护？为啥Haskell编译通过的代码基本能保证正确？？为什么需要给动态类型语言做静态分析工具？？为什么静态类型的语言有更智能的代码提示和重构工具？？为什么基于动态类型的语言开发的没有特别大型的开源项目？？为什么要在javascript之上还要再开发一个TypeScript语言用来支持大型项目的开发？？难道是闲着蛋疼？？所有的所有，都是因为，程序是类型上的证明。

AlexiaChen / AlexiaChen.github.io

什么是类型安全? #43

程序语言理论