类型安全

在计算机科学中，类型安全和类型健全是指一种编程语言阻止或防止类型错误的程度。类型安全有时也被认为是一种计算机语言设施的属性；也就是说，有些设施是类型安全的，它们的使用不会导致类型错误，而同一语言中的其他设施可能是类型不安全的，使用它们的程序可能遇到类型错误。被某个编程语言归类为类型错误的行为通常是那些试图对不属于适当数据类型的值进行操作而导致的行为，例如，在没有定义如何处理这种情况时，将一个字符串添加到一个整数中。这种分类有一部分是基于观点的。类型执行可以是静态的，在编译时捕捉潜在的错误，也可以是动态的，在运行时将类型信息与值相关联，并在需要时查询它们以检测即将发生的错误，或者两者的结合。动态类型执行通常允许程序运行，而在静态执行下，这些程序是无效的。在静态（编译时）类型系统的背景下，类型安全通常包括（除其他外）保证任何表达式的最终值将是该表达式静态类型的合法成员。精确的要求比这更微妙--例如，请参阅子类型和多态性的复杂情况。

直观地说，类型健全性是由RobinMilner的精辟论述所概括的，即类型良好的程序不会出错。换句话说，如果一个类型系统是健全的，那么该类型系统所接受的表达式必须评估为一个适当类型的值。如果一种语言中可以对数据进行的xxx操作是数据类型所认可的，那么这种语言就是类型安全的。然而，对于一个程序来说，良好的类型化或出错的确切含义是其静态和动态语义的属性，这对于每一种编程语言来说都是特定的。因此，类型健全性的精确、正式的定义取决于用于指定语言的正式语义学的风格。

一个类型良好的程序永远不会被卡住：每个表达式要么已经是一个值，要么可以以某种定义良好的方式被还原为一个值。换句话说，程序永远不会进入不可能有进一步转换的未定义状态。保存（或主题还原）在每个评价步骤之后，每个表达式的类型保持不变（也就是说，它的类型被保存了）。在指称语义学和结构性操作语义学方面，也发表了一些其他类型健全性的正式处理方法。

孤立地说，类型健全性是一个相对较弱的属性，因为它基本上只是说明类型系统的规则是内部一致的，不能被颠覆。然而，在实践中，编程语言被设计成良好的类型性也包含了其他更强的属性，其中一些包括。防止非法操作。内存安全类型系统可以防止野生指针，否则就会出现一种类型对象的指针被当作另一种类型的指针。更复杂的类型系统，例如那些支持从属类型的系统，可以检测并拒绝越界访问，防止潜在的缓冲区溢出。源于不同类型语义的逻辑错误。

一个类型系统可以为它们强制执行两种不同类型的整数。类型安全和类型不安全的语言类型安全通常是学术编程语言研究中提出的任何玩具语言（即深奥的语言）的要求。另一方面，许多语言对于人类生成的类型安全证明来说太大了，因为它们经常需要检查成千上万的情况。尽管如此，一些语言如StandardML，它有严格定义的语义，已经被证明符合类型安全的一个定义。