定义

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

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

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

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

语言的类型安全性

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

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

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

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

类型安全与强类型

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

参阅

数据类型

类型理论

免责声明：以上内容版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。感谢每一位辛勤著写的作者，感谢每一位的分享。