By Atsushi Igarashi and Benjamin C. Pierce. Information and Computation, 175(1):34-49, May 2002.
Earlier versions appered in Proceedings of the Thirteenth European Conference on Object-Oriented Programming (ECOOP'99), Springer LNCS 1628, pages 161-185, Lisbon, Portugal, June 1999 and in Proceedings of the Sixth International Workshop on Foundations of Object-Oriented Languages (FOOL 6), San Antonio, TX, January 1999
Virtual types have been proposed as a notation for generic programming in object-oriented languages---an alternative to the more familiar mechanism of parametric classes. The tradeoffs between the two mechanisms are a matter of current debate: for many examples, both appear to offer convenient (indeed almost interchangeable) solutions; in other situations, one or the other seems to be more satisfactory. It has proved difficult to draw rigorous comparisons between the two approaches, partly because current proposals for virtual types vary considerably in their details, and partly because the proposals themselves have been described rather informally, usually in the complicating context of full-scale language designs.
Work on the foundations of object-oriented languages has already established a clear connection between parametric classes and the polymorphic functions found in familiar typed lambda-calculi. Our aim here is to explore a similar connection between virtual types and dependent records.
We present, by means of examples, a straightforward model of objects with embedded type fields in a typed lambda-calculus with subtyping, type operators, fixed points, and dependent records with both ``bounded'' and ``manifest'' type fields (this combination of features can be viewed as a measure of the inherent complexity of virtual types). Using this model, we then discuss some of the major differences between previous proposals and show why some can be checked statically while others require run-time checks. We also see how the partial ``duality'' of virtual types and parametric classes can be understood in terms of translations between universal and (dependent) existential types.
Please contact me for the journal version. The previous version is not available as the formal presentation of the type system turned out to be slightly flawed.
$Date: 2005-12-24 00:27:41 +0900 (Sat, 24 Dec 2005) $