Self type constructors
Self type constructors
复制标题
DOI：
10.1145/1640089.1640109
复制
发表时间：
2009-10
期刊：
影响因子：
--
通讯作者：
C. Saito;Atsushi Igarashi
中科院分区：
文献类型：
--
作者：
C. Saito;Atsushi Igarashi
布鲁斯和福斯特提出了LOOJ语言，这是Java的一个扩展，带有MyType的概念，它表示自引用的类型，并随着继承沿着改变其含义。MyType对于为具有递归接口的对象编写可扩展但类型安全的类很有用，也就是说，具有接受或返回与接收方相同类型的对象的方法的类。虽然LOOJ也有泛型，但MyType是作为一个与泛型正交的特性引入的。因此，LOOJ不能表达递归地引用同一泛型类但使用不同类型参数的接口。这是一个重要的限制，因为这样的接口在实践中自然出现，例如，在具有方法map（）的泛型集合类中，它将集合转换为不同元素类型的同类集合。Altherr、Cremet、Moors、Piessens和Odersky给出了这个问题的解决方案，但他们使用了高级机制的高度复杂的组合，如抽象类型成员、高阶类型构造函数和F有界多态性。在本文中，我们给出了另一种解决方案，通过引入自类型构造函数，它集成了MyType和泛型，使MyType可以在泛型类中获取类型参数。自类型构造函数经过专门设计，可以比以前的解决方案更简洁地编写递归接口。通过实例说明了自类型构造函数的表达能力，形式化了一个具有自类型构造函数的核心语言，并证明了其类型安全性。
Bruce and Foster proposed the language LOOJ, an extension of Java with the notion of MyType, which represents the type of a self reference and changes its meaning along with inheritance. MyType is useful to write extensible yet type-safe classes for objects with recursive interfaces, that is, ones with methods that take or return objects of the same type as the receiver. Although LOOJ has also generics, MyType has been introduced as a feature rather orthogonal to generics. As a result, LOOJ cannot express an interface that refers to the same generic class recursively but with different type arguments. This is a significant limitation because such an interface naturally arises in practice, for example, in a generic collection class with method map(), which converts a collection to the same kind of collection of a different element type. Altherr and Cremet and Moors, Piessens, and Odersky gave solutions to this problem but they used a highly sophisticated combination of advanced mechanisms such as abstract type members, higher-order type constructors, and F-bounded polymorphism. In this paper, we give another solution by introducing self type constructors, which integrate MyType and generics so that MyType can take type arguments in a generic class. Self type constructors are tailored to writing recursive interfaces more concicely than previous solutions. We demonstrate the expressive power of self type constructors by means of examples, formalize a core language with self type constructors, and prove its type safety.