[译文]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)。

因此,我们引入ConstrainBind两个类来帮我们完成任务。

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);
}

通过找到一个合适的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>,其中ZV的子类,那么正如前文中所说的做法,我们就可以使用bind.upcast来将Z的值向上转换至V。但是,我们注意到此处Constrain的类型中带有一个通配符,因此类型系统必须推导一个类型来实现我们定义的上述限制。

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

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

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

我们可以得出以下限制:

  1. U = X – 通过归一Constrain<V, U>Constrain<V, X>
  2. WU的子类 – 通过第二个参数的类型,w必须可以被转换到U
  3. UV的子类 – 函数定义中U extends ZZ被显式指定为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)荒谬的类型

假设我们拥有一个类型VV是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社群在这个方面需要额外注意的地方。


关注微信公众号

码中人 微信公众号

发表评论

电子邮件地址不会被公开。 必填项已用*标注