类型安全

在计算机科学中，一部分编程语言具备类型安全（中国台湾用语习惯称类型为型别；依据上下文、意思、特定用语的不同，常称数据为资料）的性质。这个术语在不同的社群中有不同的定义，特别是正规的类型理论上的定义远远强过大多数的程序员的理解，但对于使用类型系统的认知，皆旨在避免必然的错误形式，和不良的程序行为（称为类型错误）。

类型错误（type error）是错误或不期望的程序行为，由不同数据类型的差别所引起，适用于程序的常量、变量、方法（函数），如把整型（int）当作了浮点型（float）。

类型安全可以静态方式实施，及早在编译时期就捕捉到潜藏的错误；或者以动态方式，在执行时期关系类型的信息，并在必要时检测即将发生的错误。类型安全是编程语言的性质，而不是程序所自有的。例如，有可能以类型不安全的语言，编写出类型安全的程序。在此是以编程语言为主，而不讨论以个人能力维护的类型安全。

某个行为之所以会被编程语言归类为类型错误，通常是因为试图对不适当类型的值进行运算。其分类的基本原则是：部分语言设计者和程序员的看法认为，如果所有运算不引起程序瓦解、安全上的瑕疵、或其它明显故障，即为合理的，而不视之为一个错误；其他人则认为所有违背程序员意图的，就是错误的，而且应该标上“不安全”。在静态类型系统中，类型安全通常包含一个保证，所有表达式最终的值都是合理的静态类型成员（比子类型和多态性所要求的还要更加精确细微）。

类型安全近似于所谓的存储器安全（就是限制从存储器的某处，将任意的字节合复制到另一处的能力）。例如，某个语言的实现具有若干类型 $t$，假如存在若干适当长度的比特，且其不为 $t$ 的正统成员。若该语言允许把那些资料复制到 $t$ 类型的变量，那个语言就不是类型安全的，因为这些运算可将非 $t$ 类型的值赋给该变量。反过来说，若该语言类型不安全的程度，最高只到允许将任意整数用作为指针，显然它就不是存储器安全的。

大部分的静态类型语言，都提供了一定程度的类型安全，而且其严格性更胜于存储器的安全性。因其类型系统强迫程序员以适当的抽象资料类型定义来使用，即使对存储器安全或任何可能的灾难而言，并不需如此严格的要求。

定义

Robin Milner 对于类型安全所喊出的口号：

“具备良好类型的程序从不出错。”

这一口号的涵义，取决于语言形式化语义的类别。在指称语义学里，类型安全意谓着一个表达式的值具有良好类型τ，则表达式是一个属于τ的集合的真正的成员。

1994年，Andrew Wright 和 Matthias Felleisen 以操作语义学定义的公式描述：何谓现今的标准定义，以及对于类型安全的检验技术。根据上述方法，类型安全是以编程语言语义中的两个性质所决定的：

藏存性

程序中的良好类型这一性质，即使转换了语言的法则（即，评价法则或约简法则），也不会有所改变。

进行性

具备良好类型的程序从不卡住，即从不进入一个使其无法进一步转换的未知状态。

这些性质不是无中生有的，而是和编程语言所描述出来的语义相连系，而且各式各样的语言存在着可以此基准来充实的广大的空间。因为“类型良好”程序的概念已是静态语义学的一部分，而“卡住”（或者“搞错”）则是动态语义学方面的属性。

语言的类型安全性

学术研究用途的玩具语言，常会提出类型安全方面的需求。另一方面，许多语言以人工方式所产生的类型安全，证实经常需要上千次的检查。不过，某些语言，如Standard ML，其严格定义了语义，且 Java 也已提供类型安全。其它语言如 Haskell 也被认为是类型安全。暂且不理会语言定义的性质，在执行时期发生的某些错误，应归于实现时的缺陷，或是用了其它语言撰写的程序库；这种错误可能使给定的实现，在某些情况下的类型不再安全。

类型安全语言的存储器管理

要实现完善的类型安全语言，它至少需要垃圾回收或增加存储器配置和解配置的限制（本节主要针对前者）。更明确地说，不允许悬置指针横跨不同结构类型的存在。这有一技术上的原因：假定类型语言（如Pascal要求分配的存储器必须显式释放）。如果存在一个仍旧指向之前的存储器地址的悬置指针，新的数据结构可能会分配到同一空间。例如，如果初始化一个指向整数区域数据结构的指针，但新对象的指针区域却分配在整数的地方，然后指针区域可借由改变整数区域的值简单改变成任可东西（经由间接引用悬置指针）。因为当指针改变时，尚未指定将会发生什么，所以这个语言就不是类型安全的。大部分类型安全的语言满足使用垃圾回收实现存储器的管理。

在允许指针算术的语言中，实现垃圾回收器是最好的，所以在类型不安全的语言或类型安全可能失效的语言中，如此实现回收器的程序库是最好的。C 和 C++ 经常使用。

类型安全与强类型

在各种强类型的定义中，其往往成为类型安全的同义词；然而，类型安全与动态类型并不互相排斥。也可将动态类型视为非常宽松的静态类型语言，而且所有语法正确的程序皆具备良好类型；只要它的动态语义学能够保证绝不会有程序“搞错”，它就可以满足上述定义，且可称为类型安全。

参阅

• 资料类型
• 类型理论

参考资料

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002. (ISBN 0-262-16209-1) [1]（页面存档备份，存于互联网档案馆）
• Type Safe defined in the Portland Pattern Repository's Wiki [2]（页面存档备份，存于互联网档案馆）
• Andrew K. Wright and Matthias Felleisen, "A Syntactic Approach to Type Soundness," Information and Computation 115(1), pp. 38-94, 1994. [3]（页面存档备份，存于互联网档案馆）
• Stavros Macrakis, "Safety and power", ACM SIGSOFT Software Engineering Notes 7:2:25 (April 1982)requires subscription