32.10 Notes

---

32.10 Notes

The first "purely functional" interpretation of objects in a typed lambda calculus was based on recursively-defined records; it introduced by Cardelli (1984) and studied in many variations by Kamin and Reddy (Reddy, 1988; Kamin and Reddy, 1994), Cook and Palsberg (1989), and Mitchell (1990a). In its untyped form, this model was used rather effectively for the denotational semantics of untyped object-oriented languages. In its typed form, it was used to encode individual object-oriented examples, but it caused difficulties with uniform interpretations of typed object-oriented languages. The most successful effort in this direction was carried out by Cook and his co-workers (Cook, Hill, and Canning, 1990; Canning, Cook, Hill, and Olthoff, 1989a; Canning, Cook, Hill, Olthoff, and Mitchell, 1989b).

Pierce and Turner (1994) introduced an encoding that relied only on a type system with existential types, but no recursive types. This led Hofmann and Pierce (1995b) to the first uniform, type-driven interpretation of objects in a functional calculus. At the same conference, Bruce presented a paper (1994) on the semantics of a functional object-oriented language. This semantics was originally presented as a direct mapping into a denotational model of , but has recently been reformulated as an object encoding that depends on both existential and recursive types. Meanwhile, frustrated by the difficulties of encoding objects in lambda calculi, Abadi and Cardelli introduced a calculus of primitive objects (1996). Later, however, Abadi, Cardelli, and Viswanathan (1996) discovered a faithful encoding of that object calculus in terms of bounded existentials and recursive types. These developments are surveyed by Bruce et al. (1999) and Abadi and Cardelli (1996).

The object encoding in this chapter has been extended to include multiple inheritance—classes with more than one superclass—by Compagnoni and Pierce (1996). The key technical idea is the extension of with intersection types (§15.7).

There have been numerous proposals for addressing the shortcomings of pure second-order bounded quantification that we observed in §32.3. Besides the two that we saw in this chapter—higher-order bounded quantification and a polymorphic record update primitive—there are several other styles of polymorphic record update (Cardelli and Mitchell, 1991; Cardelli, 1992; Fisher and Mitchell, 1996; Poll, 1996), as well as structural unfolding for recursive types (Abadi and Cardelli, 1996), positive subtyping (Hofmann and Pierce, 1995a), polymorphic repacking for existential types (Pierce, 1996), and type destructors (Hofmann and Pierce, 1998).

A different line of attack based on row-variable polymorphism has been developed by Wand (1987, 1988, 1989b), Rémy (1990, 1989, 1992), Vouillon (2000, 2001) and others, and forms the basis for the object-oriented features of OCaml (Rémy and Vouillon, 1998).

"Begin at the beginning," the King said, very gravely, "and go on till you come to the end: then stop." —Lewis Carroll

---