转载

Java 和 Scala 的类型系统是不健全的

本文作者展示了一些Java和Scala类型系统unsound的问题。

Java和Scala的类型系统使用了参数化多态（parametric polymorphism），因此允许带参数的函数根据参数来实现类型转换。作者同时指出因为JVM没有引入参数化多态，JVM不受此影响。最后，作者揭示了这样的问题在程序语言的设计上有着更大的影响。

2004年，Java 5 引入了泛型（generics）——参数化多态；同年Scala发布，发布了path-dependent type的特性。在发布之初，二者的类型系统都是不健全的。尽管诸多PL研究者对于Java的类型系统进行研究，并将其形式化，作者还是发现了Java类型系统不健全的地方。

作者指出，诸多研究者在研究一门复杂的语言的时候，选择使用一些简化的模型来进行抽象，并验证这个模型的某个核心功能，却忽视了不同的特性交织在一起的时候产生的效果。本文所发现的不健全的例子则是多个特性进行叠加之后的结果。

先上例子：

class Unsound {
  static class Constrain<A, B extends A> {}
  static class Bind<A> {
    <B extends A>
    A upcast(Constrain<A,B> constrain, B b) {
      return b;
    }
  }
  static <T,U> U coerce(T t) {
    Constrain<U,? super T> constrain = null;
    Bind<U> bind = new Bind<U>();
    return bind.upcast(constrain, t);
  } 
  public static void main(String[] args) {
    String zero = Unsound.<Integer,String>coerce(0);
  }
}

Java 8运行结果（ ClassCastException ）：

$ javac -version
javac 1.8.0_151
$ javac Unsound.java
$ java Unsound
Exception in thread "main" java.lang.ClassCastException: java.lang.Integer cannot be cast to java.lang.String
  at Unsound.main(Unsound.java:15)

Java 9运行结果（无法编译）：

$ javac -version
javac 9.0.1
$ javac Unsound.java
Unsound.java:12: error: method upcast in class Bind<A> cannot be applied to given types;
    return bind.upcast(constrain, t);
               ^
  required: Constrain<U,B>,B
  found: Constrain<U,CAP#1>,T
  reason: inference variable B has incompatible bounds
    upper bounds: U
    lower bounds: T
  where U,T,B,A are type-variables:
    U extends Object declared in method <T,U>coerce(T)
    T extends Object declared in method <T,U>coerce(T)
    B extends U declared in method <B>upcast(Constrain<A,B>,B)
    A extends Object declared in class Bind
  where CAP#1 is a fresh type-variable:
    CAP#1 extends U super: T from capture of ? super T
1 error

由于笔者不会写Scala（捂脸），所以就主要讨论Java部分了。等什么时候学会了Scala再来补一下Scala部分吧（flag）。

我们跟着作者的思路来重现这个例子的构建过程。

首先我们需要编写一个程序实现两个类之类的任意转换。

class A {}
class B {}
class Unsound {
  <V, W> V magic(W w) {
    // TODO
  }
  public static void main(String[] args) {
    Unsound u = new Unsound();
    A surprise = u.<A, B>magic(new B()); // 把B转换到A
  }
}

在 magic 方法里，我们需要一个 V 的实例，但我们只有一个 W 的实例，显然我们没有办法完成给定的任务。但是我们可以使用通配符给类型进行限制，然后进行安全的向上类型转换（upcast）。

因此，我们引入 Constrain 和 Bind 两个类来帮我们完成任务。

class Constrain<X, Y extends X> {}
class Bind<Z> {
  <U extends Z> Z
  upcast(Constrain<Z, U> constrain, U u) { return u; }
}

注意此处两个类通配符的限制：在 Constrain 类中， Y 需要是 X 的子类。在 Bind 类中，我们可以通过 Constrain 类将 U 类的实例安全的向上转换到Z类。

那么，我们可以用上面的两个类来实现我们的 magic 方法。

<V, W> V magic(W w) {
  Constrain<???> constrain = ???; //TODO
  Bind<V> bind = new Bind<V>();
  return bind.upcast(constrain, w);
}

Java 和 Scala 的类型系统是不健全的通过找到一个合适的 Constrain 类实例和参数，我们可以通过 Bind 类将 W 类向上转换到 V 类，那么剩下要做的就是找出合适的参数了。

我们假定 Constrain 类的参数为 <T1, T2> ，值为 val 。那么我们需要寻找的则是使下列条件满足的实例：

Constrain<T1, T2> 是一个合法的类型
bind.upcast 可以通过类型检查
val 满足 Constrain<T1, T2> 的类型限制

我们选择

Constrain<V, ? super W> constrain = null;

来满足上述要求。

首先， Constrain<V, ? super W> 是一个合法的类型，这个类型中使用了一个带下界的通配符。通过 ? super W ，我们得知通配符类型是 W 的母类；又因为定义中要求的 Y extends X ，所以通配符类型是 V 的子类。在检查类型是否合法时，并不会检查是否有类型实例能满足给定的限制，因此使用通配符可以让我们避免给定一个满足限制的实例。

我们其次考虑 bind.upcast 。我们显式地定义了 Bind 类的类型参数为 V ，因此假设 Constrain 的类型参数为 <V, Z> ，其中 Z 是 V 的子类，那么正如前文中所说的做法，我们就可以使用 bind.upcast 来将 Z 的值向上转换至 V 。但是，我们注意到此处 Constrain 的类型中带有一个通配符，因此类型系统必须推导一个类型来实现我们定义的上述限制。

类型系统的推导过程由收集所有对于类型的假设和必需的要求开始，其次试图找到一个满足限制的类型。

我们假设需要推导的通配符类型为 X 。从上文我们得知， X 是 W 的母类，是 V 的子类。

在定义中， bind.upcast 的第一个参数的类型为 Constrain<V, U> （显式指定了 Z 为 V ），实际类型为 Constrain<V, X> 。第二个参数的类型为 U ，实际类型为 W 。

我们可以得出以下限制：

U = X – 通过归一 Constrain<V, U> 和 Constrain<V, X>
W 是 U 的子类 – 通过第二个参数的类型， w 必须可以被转换到 U 类
U 是 V 的子类 – 函数定义中 U extends Z ， Z 被显式指定为 V

因为有限制（1）的存在，我们将限制（2）（3）中的U替换成X。在类型推导中，通配符给定的限制并不是限制，而是假设。因此限制（2）（3）可以被通配符类型来满足，所以 bind.upcast 可以通过类型检查。

另外需要注意的是，尽管Java的类型参数推导是不可决定的（undecidable），Java 8的编译器成功地编译了上面的代码，而Java 9却无法编译。作者提到了类型推导是不确定的（non-deterministic），并认为Java 9先考虑了限制（2）（3）。由于子类关系是传递性的，那么 W 必须是 V 的子类，而这个关系是不满足的，因此发生了编译错误。作者后续给出了其他Java 9的例子，可以通过编译，但是在运行时会抛出异常。（传送门里有其他例子）

第三步，则是找到一个合适的值。如果说我们没有办法提供一个 constrain 的值，那么上面的例子就没有办法实现我们需要的功能。但是我们需要注意到，假设我们需要给定这个值，我们必须要找到一个类型来满足通配符中所要求的子类关系（即通配符中的类型是 W 的母类，是 V 的子类），可这是没有办法做到的。幸运的是/不幸的是，在Java里， null 可以做任何引用类型的值。在这一步，我们就可以跳过寻找通配符类型的过程，但仍然通过类型检查。

至此，我们成功的构造了在Java类型系统容许下的任意类型之间的相互转换。

作者分三方面来阐述这个例子带来的启示：

（1）荒谬的类型

假设我们拥有一个类型 V ， V 是Top type的supertype，亦是Bottom type的subtype，那么我们即可通过此类型 V 来实现任何类型之间的转换，如：

String <: Top <: V <: Bottom <: Integer

然而作者指出，使用算法来鉴别荒谬的类型是非常困难的。由于subtyping需要算法来实现，而类型验证亦需要算法实现。要成功地识别出荒谬的类型，二者之间会存在一些需要解决的循环依赖，给实现增加难度。

（2） null —— the billion dollar mistake

作者指出了 null 在类型系统的中潜在的危害性。随着类型系统的逐步成熟， null 的存在会给设计者带来更多需要考虑的地方。在本文中的例子里，我们通过 null 来跳过重要的推导步骤，实现任意类型之间的转换。在Java中 null 可以表示任何引用类型的值，在设计类型规则的时候，需要在此加以注意。

（3）没有预见的特性交互

作者指出了对于一门被众多人使用、特性丰富的语言，研究者很难做到将每个功能都正规化，然后将其验证。因此诸多研究者把Java的语言的核心部分形式化，并逐步迭代加入新的特性。但是在将Java语言取核心部分最小化成形式语言的过程中，会不会遗漏一些特性，使其与其他特性交互时，产生没有预见的效果。作者在此段从方法、验证、价值观和审阅、发表流程的角度来反思PL社群在这个方面需要额外注意的地方。

原文 http://www.techug.com/post/java-and-scalas-type-systems-are-unsound.html

正文到此结束