0 简介

在编程语言中拥有类型有两个主要后果：

1,允许对值执行的操作;2,位序列的解释

对于第一个结果某个类型的值仅支持应用于此类型的操作。因此，如果我们考虑整数类型，那么这些运算将包括加法、减法等。
另一方面，对于字符类型，操作将包括转换为大写字母

对于第二个结果，内存中的位序列具有依赖于此类型的解释。例如，位序列 0010 1011。
如果它的类型为“integer”，则为值 43。但是，如果字符类型为“character”，则相同的位序列是字符“+”

静态类型在编译时确保类型安全，保守地避免不良行为，如if test; then 5 else ;error ;会被拒绝，即便运行时可能正确。

动态类型语言在运行时检查，可能允许更多灵活性但可能导致运行时错误。类型系统设计平衡保守性与表现力，用于模块化和抽象保护。类型注释能增强类型检查，有时可转化为证明检查器。

类型是一组值。例如，我们可能有一种称为“8 位整数”的类型。这是从 -128 到 127 的所有整数的集合。

换句话说，它是由 8 位组成的所有整数值的集合。再举一个例子，我们可能有一个名为“8 位字符”的类型。
例如，这些可能是英文字母、数字和一些特殊字符的字母

1 更抽象的焦点，静态和动态

关于各种“纯类型λ演算”和变体之间的逻辑联系，两个都使用相似的概念、符号和技术，但在方向上有一些重要的差异。例如，对类型化 lambda 演算的研究。

通常关注的系统中，每一个类型良好的计算都是保证终止，而大多数编程语言都牺牲了这一点属性，以实现递归函数定义等功能。

上述定义中的另一个重要元素是它强调根据执行时将计算的值的属性对术语（句法短语）进行分类。

可以认为一个类型系统,作为计算运行时行为的一种静态近似程序中的条款。 （此外，分配给术语的类型通常是组合计算的，表达式的类型仅取决于其子表达式的类型。）

有时会显式添加“静态”一词——例如，我们说的是“静态类型编程语言”——以区分类别在编译时分析中，我们正在从诸如 Scheme 等语言中发现的动态或潜在类型中考虑（Sussman and Steele, 1975;Kelsey, Clinger, and Rees, 1998; Dybvig, 1996)，其中运行时类型标签是用于区分堆中不同种类的结构。

像“动态类型”这样的术语可以说是用词不当，应该被替换为“动态检查”，但用法是标准的。

作为静态的，类型系统也必然是保守的：它们可以明确地证明不存在某些不良程序行为，但它们不能证明他们的存在，因此他们有时也必须拒绝程序实际上在运行时表现良好。

例如，像这样的程序

    if <complex test> then 5 else <type error>

将被拒绝为错误类型，即使碰巧 将总是评估为真，因为静态分析无法确定这是这样的。保守性和表现力之间的张力是类型系统设计中的一个基本事实。

允许更多的愿望要键入的程序——通过为它们的部分分配更准确的类型——是推动该领域研究的主要力量。

相关的一点是，相对简单的分析体现在大多数类型系统不能禁止任意不受欢迎的程序行为；他们只能保证类型良好的程序是免费的来自某些类型的不当行为。

例如，大多数类型系统可以检查静态地，原始算术运算的参数总是数字，方法调用中的接收者对象总是提供请求的方法等，但不是除法的第二个参数操作非零，或者数组访问总是在界限内。

可以通过给定语言中的类型系统消除的不良行为通常称为运行时类型错误。

记住这一点很重要这组行为是每种语言的选择：尽管在被认为是运行时类型错误的行为之间存在大量重叠不同的语言，原则上每个类型系统都有一个定义它旨在防止的行为。

每种类型的安全性（或健全性）必须根据自己的一组运行时错误来判断系统。

类型分析检测到的不良行为种类不限于低级错误，例如调用不存在的方法：类型系统也是用于强制执行更高级别的模块化属性并保护用户定义的抽象的完整性。

违反信息隐藏，例如因为直接访问其表示应该是抽象的数据值的字段，是运行时类型错误，其方式与以下完全相同：

    例如，将整数视为指针并使用它来使机器崩溃。

类型检查器通常内置在编译器或链接器中。这意味着他们必须能够自动完成工作，无需人工干预或与程序员的交互——即，它们必须体现计算上易于处理的分析。

但仍有很大的要求空间程序员的指导，以显式类型注释的形式程式。

2 小结

通常，这些注释的保持简单相当不容易，它们的存在以制作程序更容易书写和阅读。

但是，原则上，该程序符合一些任意规范可以编码在类型注释中；

在这在这种情况下，类型检查器将有效地成为一个证明检查器。比如使用扩展静态检查等技术（Detlefs、Leino、Nelson 和 Saxe，1998 年）

正在努力解决类型系统和全面的程序验证方法之间的这一领域，对一些实施全自动检查仅依赖于“轻度合理”的广泛类别的正确性属性程序注释来指导他们的工作。

甚至像 ML 这样广泛使用的类型系统（Damas 和 Milner，1982 年）可能在病理案例中表现出巨大的类型检查时间成本（Henglein和迈尔森，1991）。

有些语言具有无法确定的类型检查或类型重构问题，比如对于哪些算法是可在“大多数实际感兴趣的情况下”立刻停止。

出于同样的原因，我们最感兴趣的方法不仅仅是原则上是可自动化的，实际上也带有高效的算法用于检查类型。然而，究竟什么才是最有效的，仍然在辩论。

参考：

  皮尔斯 和特纳(Pierce and Turner)，2000；
  纳达瑟和米勒(Nadathur and Miller)，1988；
  普芬宁(Pfenning)，1994。