F-bounded polymorphism for object-oriented programming

authors: Peter Canning, William Cook, Walter Hill, Walter Olthoff, John C Mitchell
year: 1989
url: https://dl.acm.org/doi/10.1145/99370.99392
publisher: ACM Press
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.