Extensible records in the System E Framework and a new approach to object-oriented type inference
- Publication Type:
- Thesis
- Issue Date:
- 2013
Open Access
Copyright Clearance Process
- Recently Added
- In Progress
- Open Access
This item is open access.
Extensible records were proposed by Wand as a foundation for studying object-oriented type inference. One of their key benefits is that they allow for an elegant encoding of object-oriented inheritance, where one class of objects may be defined as an extension of another class of objects. However, every system of type inference designed for extensible records to date has been developed in the Hindley/Milner-style, a consequence being that polymorphism in these systems is not first-class and analysis is not strictly compositional. We argue that both of these features are necessary to retain the modelling and engineering benefits of traditional object-oriented languages such as Java:
1. Object-oriented modelling depends on the treatment of objects as first-class citizens, and this demands a type inference system capable of handling first-class polymorphism.
2. Object-oriented engineering encourages the separate development of software modules, and this should be supported by the type inference system with compositional analysis.
Both of these features are present in a type system for the λ-calculus called System E, which supports first-class polymorphism via intersection types, and compositional type inference via expansion variables. However, research into System E has so far focused on refining and simplifying the formulation of expansion variables and exploring type inference algorithms with various properties. Meanwhile, the system has not yet been extended beyond the terms of the pure λ-calculus and it lacks many features that would be needed in a practical object-oriented language.
In this dissertation, we combine System E with Wand’s extensible records resulting in a new approach to type inference for extensible records that better preserves the modelling and engineering benefits of object orientation stated above. The resulting system, called System Evcr, is significant because previous type inference systems, both for extensible records in particular, and also for object orientation in general, have at best preserved only one or the other of these two benefits, but never both of them simultaneously. System Evcr also makes a significant contribution to the work on System E, since it demonstrates for the first time that the System E’s expansion variables can be adapted to analyse programs whose term language extends beyond the pure λ-calculus.
To demonstrate the potential use of System Evcr in object-oriented type inference, an implementation of our type inference algorithm was created and is shown to succeed on problem examples that previous systems either fail to analyse, or else fail to analyse compositionally.
Please use this identifier to cite or link to this item: