Principles of Object-Oriented Software Development
[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources

talk show tell print


This chapter has treated polymorphism from a foundational perspective. In section 1, we looked at abstract inheritance as employed in knowledge representation.

Abstract inheritance


slide: Section 9.1: Abstract inheritance

We discussed the non-monotonic aspects of inheritance networks and looked at a first order logic interpretation of taxonomic structures.

The subtype relation


  • types -- sets of values
  • the subtype relation -- refinement rules
  • functions -- contravariance
  • objects -- as records

slide: Section 9.2: The subtype relation

In section 2, a characterization of types as sets of values was given. We looked at a formal definition of the subtype relation and discussed the refinement rules for functions and objects.

Flavors of polymorphism


  • typing -- protection against errors
  • flavors -- parametric, inclusion, overloading, coercion
  • inheritance -- incremental modification mechanism

slide: Section 9.3: Flavors of polymorphism

In section 3, we discussed types as a means to prevent errors, and distinguished between various flavors of polymorphism, including parametric polymorphism, inclusion polymorphism, overloading and coercion. Inheritance was characterized as an incremental modification mechanism, resulting in inclusion polymorphism.

Type abstraction


  • subtypes -- typed lambda calculus
  • overloading -- intersection types
  • bounded polymorphism -- generics and inheritance

slide: Section 9.4: Type abstraction

In section 4, some formal type calculi were presented, based on the typed lambda calculus. These included a calculus for simple subtyping, a calculus for overloading, employing intersection types, and a calculus for bounded polymorphism, employing type abstraction. Examples were discussed illustrating the (lack of) features of the C++ type system.

Existential types


  • hiding -- existential types
  • packages -- abstract data types

slide: Section 9.5: Existential types

In section 5, we looked at a calculus employing existential types, modeling abstract data types and hiding by means of packages and type abstraction.



  • self-reference -- recursive types
  • object semantics -- unrolling
  • inheritance -- dynamic binding
  • subtyping -- inconsistencies

slide: Section 9.6: Self-reference

Finally, in section 6, we discussed self-reference and looked at a calculus employing recursive types. It was shown how object semantics may be determined by unrolling, and we studied the semantic interpretation of dynamic binding. Concluding this chapter, an example was given showing an inconsistency in the Eiffel type system.


  1. How would you characterize inheritance as applied in knowledge representation? Discuss the problems that arise due to non-monotony.
  2. How would you render the meaning of an inheritance lattice? Give some examples.
  3. What is the meaning of a type? How would you characterize the relation between a type and its subtypes?
  4. Characterize the subtyping rules for ranges, functions, records and variant records. Give some examples.
  5. What is the intuition underlying the function subtyping rule?
  6. What is understood by the notion of objects as records? Explain the subtyping rule for objects.
  7. Discuss the relative merits of typed formalisms and untyped formalisms.
  8. What flavors of polymorphism can you think of? Explain how the various flavors are related to programming language constructs.
  9. Discuss how inheritance may be understood as an incremental modification mechanism.
  10. Characterize the simple type calculus %l_{<=}, that is the syntax, type assignment and refinement rules. Do the same for F_{ /\ } and F_{<=}.
  11. Type the following expressions: (a) { a = 1, f = %l x:Int. x + 1 }, (b) %l x:Int . x * x , and (c) %l x:{ b:Bool, f:{ a:Bool } } -> Int.x.f(x) .
  12. Verify whether: (a) f' : 2..5 -> Int <= f:1..4 -> Int, (b) { a:Bool, f:Bool -> Int } <= { a:Int, f: Int -> Int }, and (c) %l x: { a:Bool } -> Int <= %l x: { a:Bool, f:Bool -> Int } -> Int.
  13. Explain how you may model abstract data types as existential types.
  14. What realizations of the type \E %a. { a:%a, f:%a -> Bool } can you think of? Give at least two examples.
  15. Prove that %m %a . { c:%a, b:%a -> %a } \not<= %m %a . { b : %a -> %a } .
  16. Prove that %m %a . { c : %a, b: %t -> %a } <= %t , for %t = %m %a.{ b: %a -> %a }.

slide: Questions

Further reading

As further reading I recommend  [CW85] and  [Pierce93]. As another source of material and exercises consult  [Palsberg94].  [BG93] contains a number of relevant papers. An exhaustive overview of the semantics of object systems, in both first order and second order calculi, is further given in  [ObjectCalculus].

[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources

draft version 0.1 (15/7/2001)