java类型系统介绍

原文链接

首先是对参数化多态的扩展，支持给泛型变量添加边界，即：<T extends X>等，这样可以表示更加精确的类型约束，而不仅仅是 forall；不仅如此，Java 还支持 F-bounded，即类型变量可以出现在自己的上边界中：<T extends F<T>>

class Test {
  public static void main(String[] args) {
    Comparable<String> a = min("cat", "dog");
    Comparable<Integer> b = min(new Integer(10), new Integer(3));
    String str = Fmin("cat", "dog");
    Integer i = Fmin(new Integer(10), new Integer(3));
  }
  public static <S extends Comparable> S min(S a, S b) {
    if (a.compareTo(b) <= 0)
      return a;
    else
      return b;
  }
  public static <T extends Comparable<T>> T Fmin(T a, T b) {
    if (a.compareTo(b) <= 0)
      return a;
    else
      return b;
  }
}

注意 Fmin 方法的 <T extends Comparable<T>>，如果Comparable 不能包含 T，即像 min 方法那样，就会丢失接口 Comparable compareTo 方法的参数类型 (变成 Object)，你会收到一个编译器的警告，说你绕过了编译检查直接使用了 raw type（参数化类型擦除后的类型）；详情可参考 F-bounded quantification

引入了 wildcards，List<? extends Integer> 就是 List<? extends Number> 的子类（详情参考Wildcards and Subtyping)

1	typeof: (Γ, e) -> t

大写希腊字母 Γ 用于表示当前上下文（typing context, aka typing environment），它就是一个类型绑定关系的 Map，保存了项的类型（即：e 到 t），e 为表达式的 AST（抽象语法树），t 为类型（具体实现时也是一类特殊的 AST 节点），typeof 在数学上的写法为：Γ ├ e: t 读作：在类型上下文 Γ 下，e 的类型为 t；符号 ‘├’ 在数学上是推导，推断的意思，它在这是一种三元关系即：HasType(Γ, e, t)。

所以只要在当前上下文下，语法项有具体类型，则类型检查就通过，如果无法返回其类型，那么就报错了，也就是我们常常看到的编译不过。

类型是什么呢？有两种不同的角度，一种是计算的角度（程序员的角度）或者称 Church 的角度，另一种是逻辑的角度，或者叫 Curry 的角度；前者根据所计算的值的性质来对项（语法项）进行分类，你可以把类型比作集合；后者就是对程序行为进行证明的推理工具，所以类型理论常常和证明理论扯上关系。

####类型系统

Lambda 演算可以看做是一门微小的函数式编程语言，它的语法构造非常简单，只有变量，函数(aka 抽象)，和函数应用（调用）：

<expr> ::= <name> | <function> | <application>
<function> ::= λ<name>.<body>
<body> ::= <expr>
<application> ::= (<expr> <expr>)

主要是利用函数部分，利用函数式编程中的，一切皆函数

STLC (Simply Typed Lambda calculus)

就是在无类型的 Lambda 演算基础上添加了类型，其语法结构（BNF）：

types:
τ ::= α        base type
    | τ → τ'   function type

terms:
e ::= e : τ    annotated term type τ
    | x        variable
    | (e e')   application
    | λx.e     lambda abstraction