Summary

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

Abstract inheritance

abstract inheritance -- declarative relation
inheritance networks -- non-monotonic reasoning
taxonomic structure -- predicate calculus

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

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.

Questions

How would you characterize inheritance as applied in knowledge representation? Discuss the problems that arise due to non-monotony.
How would you render the meaning of an inheritance lattice? Give some examples.
What is the meaning of a type? How would you characterize the relation between a type and its subtypes?
Characterize the subtyping rules for ranges, functions, records and variant records. Give some examples.
What is the intuition underlying the function subtyping rule?
What is understood by the notion of objects as records? Explain the subtyping rule for objects.
Discuss the relative merits of typed formalisms and untyped formalisms.
What flavors of polymorphism can you think of? Explain how the various flavors are related to programming language constructs.
Discuss how inheritance may be understood as an incremental modification mechanism.
Characterize the simple type calculus $%l_{<=}$ , that is the syntax, type assignment and refinement rules. Do the same for $F_{ /\ }$ and $F_{<=}$ .
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)$ .
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$ .
Explain how you may model abstract data types as existential types.
What realizations of the type $\E %a. { a:%a, f:%a -> Bool }$ can you think of? Give at least two examples.
Prove that $%m %a . { c:%a, b:%a -> %a } \not<= %m %a . { b : %a -> %a }$ .
Prove that $%m %a . { c : %a, b: %t -> %a } <= %t$ , for $%t = %m %a.{ b: %a -> %a }$ .

slide: Questions