F-Bounded Polymorphism for Object-Oriented Programming

Abstract

Bounded quantification was introduced by Cardelli and Wegner as a means of typing functions that operate uniformly over all subtypes of a given type. They defined a simple “object” model and used bounded quantification to type-check functions that make sense on all objects having a specified set of “attributes.” A more realistic presentation of object-oriented languages would allow objects that are elements of recursively-defined types. In this context, bounded quantification no longer serves its intended purpose. It is easy to find functions that makes sense on all objects having a specified set of methods, but which cannot be typed in the Cardelli-Wegner system. To provide a basis for typed polymorphic functions in object-oriented languages, we introduce F-bounded quantification. Some applications of F-bounded quantification are presented and semantic issues are discussed. Although our original motivation was to type polymorphic functions over objects, F-bounded quantification is a general form of polymorphism that seems useful whenever recursive type definitions and subtyping are used.

Introduction

Although object-oriented programming has attracted increasing interest in recent years, the development of polymorphic type systems for object-oriented languages has progressed slowly. One reason is that object-oriented languages are often described using terminology that sets them apart from functional languages. In addition, there has been a lack of formal models for object-oriented languages. As a result, it has been dificult to see how practical polymorphic type systems should be adapted for typing object-oriented constructs. In Cardelli’s seminal paper [8], record subtyping was identified as an important form of polymorphism in object-oriented programs. This lead to the development of “bounded quantification” in [7]. If we view objects as elements of non-recursive record types, then bounded quantification provides a useful form of polymorphism over objects. However, a more sophisticated presentation of object-oriented constructs (as in [5, 11, 10]) would allow objects that are elements of recursively-defined types. With recursive types, the Cardelli-Wegner form of bounded quantification is not sufficiently expressive to meet its original goal.

Download file here