类型检查

类型系统

类型系统给每一个组成部分赋予一个类型表达式，通过一组逻辑规则来表达类型表达式必须满足的条件，可以发现错误、提高代码效率、确定临时变量的大小。

• 强类型/弱类型：根据类型互操作性/类型系统严格性区分。强类型不允许无关类型数据间的操作，弱类型通过隐式类型转换，允许无关类型间的操作。

• 静态类型/动态类型：根据类型检查时机区分。

  • 静态类型：静态（编译期）进行类型检查

  • 动态类型：动态（运行时）进行类型检查

  • Gradual Typing：混合，部分静态，部分动态

  

类型规则（Type Inference Rule）

用分式记法表达推导规则：

类型判决式（type judgement）：读作表达式e的类型为T

$$e:T$$

无条件成立的规则：

简洁（易读易写）；抽象（通用，独立于具体语言）

标识符的类型规则

为了推导标识符相关的类型，需要在类型规则中引入上下文，通常用Γ表示（也称作类型环境）。

$$\Gamma \vdash e: T$$

读作在上下文Γ中，表达式e的类型是T。

函数/运算符的重载

通过查看参数来解决函数重载问题：

char foo(int x) { … }
boolean foo(float x) { … }
int bar(int p ) {
    …
    n = foo(p);
    …
}

类型转换

假设在表达式x*i 中，x为浮点数，i为整数，则结果应该是浮点数。x和i使用不同的二进制表示方式，浮点乘法和整数乘法使用不同的指令。

类型转换比较简单时的SDT

类型拓宽（widening）和窄化（narrowing）：

Java的类型转换规则，编译器自动完成的转换为隐式转换，程序员用代码制定的转换为显式转换。

拓宽通常不丢失信息，窄化有可能丢失信息。

处理类型转换的SDT

函数max求出两个参数在拓宽层次结构中的最小公共祖先，函数widen生成必要的类型转换代码。

widen函数