topical media & game development
[] readme course(s) preface I 1 2 II 3 4 III 5 6 7 IV 8 9 10 V 11 12 afterthought(s) appendix reference(s) example(s) resource(s) _

talk show tell print

object-oriented programming

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

Polymorphism

From a theoretical perspective, object orientation may be characterized as combining abstract data types and polymorphism. These notions may be considered as the theoretical counterparts of the more operational notions of encapsulation and inheritance.

Polymorphism

9


Additional keywords and phrases: exceptions, type calculi, parametric types, coercion, ad hoc polymorphism, universal types, existential types, unfolding, intersection types

slide: Polymorphism
In this chapter we will study the notion of polymorphism. We start our exploration by looking at the role of inheritance in knowledge representation. Then we will formally characterize the (signature) subtype relation and explain the contravariance rule for function subtypes. To better understand polymorphism and its relation to inheritance, we will develop a type calculus, allowing us to define abstract types using universally and existentially quantified type expressions. In a similar way, we will look at polymorphism due to overloading and generic type definitions. Finally, we will look at the role of self-reference in typing object descriptions derived by inheritance. Together with developing the calculi, examples will be given that illustrate the properties of the C++ and Eiffel type systems.

object-oriented programming

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

Abstract inheritance

Inheritance hierarchies play a role both in knowledge representation systems and object-oriented programming languages, see  [LNS90]. In effect, historically, the notions of frames and is-a hierarchies (that play a role in knowledge representation) and the notions of classes and inheritance (that have primarily been developed in a programming language context) have mutually influenced each other. In object-oriented programming languages, classes and inheritance are strongly related to types and polymorphism, and directed towards the construction of reliable programming artifacts. In contrast, the goal of knowledge representation is to develop a semantically consistent description of some real world domain, which allows us to reason about the properties of the elements in that domain.

Abstract inheritance

  • declarative relation among entities

Inheritance networks

  • isa-trees -- partial ordering
  • isa/is-not -- bipolar, is-not inference

Non-monotonic reasoning


    Nixon is-a Quaker
    Nixon is-a Republican
    Quakers are Pacifists
    Republicans are not Pacifists

Incremental system evolution is in practice non-monotonic!

slide: Knowledge representation and inheritance
One of the first formal analyses of the declarative aspects of inheritance systems was given in  [To86]. The theoretical framework developed in  [To86] covers the inheritance formalisms found in frame systems such as FRL, KRL, KLONE and NETL, but also to some extent the inheritance mechanisms of Simula, Smalltalk, Flavors and Loops. The focus of  [To86], however, is to develop a formal theory of inheritance networks including defaults and exceptions. The values of attributes play a far more important role in such networks than in a programming context. In particular, to determine whether the relationships expressed in an inheritance graph are consistent, we must be able to reason about the values of these attributes. In contrast, the use of inheritance in programming languages is primarily focused on sharing instance variables and overriding (virtual) member functions, and is not so much concerned with the actual values of instance variables. Inheritance networks in knowledge representation systems are often non monotonic as a result of having is-not relations in addition to is-a relations and also because properties (for example can-fly) can be deleted. Monotonicity is basically the requirement that all properties are preserved, which is the case for strict inheritance satisfying the substitution principle. It is a requirement that should be adhered to at the risk of jeopardizing the integrity of the system. Nevertheless, strict inheritance may be regarded as too inflexible to express real world properties in a knowledge representation system.

The meaning of is-a and is-not relations in a knowledge representation inheritance graph may equivalently be expressed as predicate logic statements. For example, the statements

  • \A x . Quaker(x) -> Human(x)
  • \A x . Republican(x) -> Human(x)
express the relation between, respectively, the predicates Quaker and Republican to the predicate Human in the graph above. In addition, the statements
  • \A x . Quaker(x) -> Pacifist(x)
  • \A x . Republican(x) -> \neg Pacifist(x)
introduce the predicate Pacifist that leads to an inconsistency when considering the statement that Nixon is a Quaker and a Republican. Some other examples of statements expressing relations between entities in a taxonomic structure are given in slide 9-logic.

Taxonomic structure


   \A x . Elephant(x) -> Mammal(x) 
   \A x . Elephant(x) -> color(x) = gray 
   \A x . Penguin(x) -> Bird(x) /\ \neg CanFly(x)
slide: Taxonomies and predicate logic
 The latter is often used as an example of non-monotonicity that may occur when using defaults (in this case the assumption that all birds can fly). The mathematical semantics for declarative taxonomic hierarchies, as given in  [To86], are based on the notion of constructible lattices of predicates, expressing a partial order between the predicates involved in a taxonomy (such as, for example, Quaker and Human). A substantial part of the analysis presented in  [To86], however, is concerned with employing the graph representation of inheritance structures to improve on the efficiency of reasoning about the entities populating the graph. In the presence of multiple inheritance and non-monotonicity due to exceptions and defaults, care must be taken to follow the right path through the inheritance graph when searching for the value of a particular attribute. Operationally, the solution presented by  [To86] involves an ordering of inference paths (working upwards) according to the number of intermediate nodes. Intuitively, this corresponds to the distance between the node using an attribute and the node defining the value of the attribute. In strictly monotonic situations such a measure plays no role, however!

object-oriented programming

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

The subtype relation

subsections:

In this section, we will study the subtype relation in a more formal manner. First we investigate the notion of subtypes in relation to the interpretation of types as sets, and then we characterize the subtype relation for a number of constructs occurring in programming languages (such as ranges, functions and records). Finally, we will characterize objects as records and correspondingly define the subtype relation for simple record (object) types. These characterizations may be regarded as a preliminary to the type calculi to be developed in subsequent sections.

Types as sets

A type, basically, denotes a set of elements. A type may be defined either extensionally, by listing all the elements constituting the type, or descriptively, as a constraint that must be satisfied by an individual to be classified as an element of the type.

Types as sets of values

  • V \approx Int \cup ... \cup V \times V \cup V -> V

Ideals -- over $V$

  • subtypes -- ordered by set inclusion
  • lattice -- Top = V, Bottom = \emptyset

Type system

subtypes correspond to subsets


  • a collection of ideals of V
slide: The interpretation of types as sets
 Formally, we may define the value set of a type with subtypes as an isomorphism of the form 

  V \approx Int  \cup ... \cup   V \times V  \cup  V -> V
which expresses that the collection of values V consists of (the union of) basic types (such as Int) and compound types (of which V itself may be a component) such as record types (denoted by the product V \times V) and function types (being part of the function space V -> V). Within this value space V, subtypes correspond to subsets that are ordered by set inclusion. Technically, the subsets corresponding to the subtypes must be ideals, which comes down to the requirement that any two types have a maximal type containing both (in the set inclusion sense). Intuitively, the subtype relation may be characterized as a refinement relation, constraining the set of individuals belonging to a type. The subtype refinement relation may best be understood in terms of improving our knowledge with respect to (the elements of) the type. For a similar view, see  [GO90]. In case we have no knowledge of a particular element we simply (must) assume that it belongs to the value set V. Having no knowledge is represented by the maximal element of the lattice Top, which denotes the complete set V. Whenever we improve our knowledge, we may be more specific about the type of the element, since fewer elements will satisfy the constraints implied by our information. The bottom element Bottom of our type lattice denotes the type with no elements, and may be taken to consist of the elements for which we have contradictory information. See slide 9-types. Mathematically, a type system is nothing but a collection with ideals within some lattice V. In our subsequent treatment, however, we will primarily look at the refinement relation between two elements, rather than the set inclusion relation between their corresponding types.

The subtype refinement relation

In determining whether a given type is a subtype of another type, we must make a distinction between simple (or basic) types built into the language and compound (or user-defined) types explicitly declared by the programmer. Compound types, such as integer subranges, functions, records and variant records, themselves make use of other (basic or compound) types. Basic types are (in principle) only a subtype of themselves, although many languages allow for an implicit subtyping relation between for example integers and reals. The rules given in slide 9-subtypes characterize the subtyping relation for the compound types mentioned.

Sub-range inclusion

<=


  • \ffrac{n <= n' and m' <= m}{n'..m' <= n..m}

Functions

contravariance


  • \ffrac{ %s <= %s' and %t' <= %t}{%s' -> %t' <= %s -> %t }

Records

  • \ffrac{ %s_i <= %t_i for i = 1..m (m <= n) }{ {a_1: %s_1, ... , a_n: %s_n} <= {a_1: %t_1 , ... , a_m: %t_m} }

Variants

  • \ffrac{%s_i <= %t_i for i = 1..m (m <= n) }{ [a_1:%s_1 \/ ... \/ a_m:%s_m] <= [a_1:%t_1 \/ ... \/ a_n:%t_n] }
slide: The subtype refinement relation
 We use the relation symbol <= to denote the subtype relation. Types (both basic and compound) are denoted by %s and %t. For subranges, a given (integer) subrange %s is a subtype of another subrange %t if %s is (strictly) included in %t as a subset. In other words, if %s = n'..m' and %t = n..m then the subtyping condition is n <= n' and m' <= m. We may also write n'..m' \subseteq n..m in this case. For functions we have a somewhat similar rule, a function f' : %s' -> %t' (with domain %s' and range or codomain %t') is a subtype of a function f : %s -> %t (with domain %s and codomain %t) if the subtype condition %s <= %s' and %t' <= %t is satisfied. Note that the relation between the domains is contravariant, whereas the relation between the ranges is covariant. We will discuss this phenomenon of contravariance below. Records may be regarded as a collection of labels (the record fields) that may have values of a particular type. The subtyping rule for records expresses that a given record (type) may be extended to a (record) subtype by adding new labels, provided that the types for labels which occur in both records are refined in the subtype. The intuition underlying this rule is that by extending a record we add, so to speak, more information concerning the individuals described by such a record, and hence we constrain the set of possible elements belonging to that (sub)type. Variants are (a kind of) record that leave the choice between a (finite) number of possible values, each represented by a label. The subtyping rules for variants states that we may create a subtype of a given variant record if we reduce the choice by eliminating one or more possibilities. This is in accord with our notion of refinement as improving our knowledge, since by reducing the choice we constrain the set of possible individuals described by the variant record. The subtyping rules given above specify what checks to perform in order to determine whether a given (compound) type is a subtype of another type. In the following we will look in more detail at the justification underlying these rules, and also hint at some of the restrictions and problems implied. However, let us first look at some examples. See slide 9-ex-subtyping.

Examples

subtyping


  • 8..12 -> 3..5 <= 9..11 -> 2..6
  • { age : int, speed : int, fuel : int } <= { age : int, speed : int }
  • [ yellow \/ blue ] < [ yellow \/ blue \/ green ]
slide: Examples of subtyping
 As a first example, when we define a function f' : 8..12 -> 3..5 and a function f : 9..11 -> 2..6 then, according to our rules, we have f' <= f. Recall that we required subtypes to be compatible with their supertypes, compatible in the sense that an instance of the subtype may be used at all places where an instance of the supertype may be used. With regard to its signature, obviously, f' may be used everywhere where f may be used, since f' will deliver a result that falls within the range of the results expected from f and, further, any valid argument for f will also be accepted by f' (since the domain of f' is larger, due contravariance, than the domain of f). As another example, look at the relation between the record types { age : int, speed : int, fuel : int } and { age : int, speed : int }. Since the former has an additional field fuel it delimits so to speak the possible entities falling under its description and hence may be regarded as a subtype of the latter. Finally, look at the relation between the variant records [yellow : color \/ blue : color ] and [yellow : color \/ blue : color \/ green : color ]. The former leaves us the choice between the colors yellow and blue, whereas the latter also allows for green objects and, hence, encompasses the set associated with [yellow : color \/ blue : color ].

Contravariance rule

The subtyping rules given above are all rather intuitive, except possibly for the function subtyping rule. Actually, the contravariance expressed in the function subtyping rule is somewhat of an embarrassment since it reduces the opportunities for specializing functions to particular types. See slide 9-functions.

Function refinement

  • f' : Nat -> Nat \not<= f : Int -> Int

Functions -- as a service

contravariance


  • domain -- restrictions for the client
  • range -- obligations for server
slide: The function subtype relation
 Consider, for example, that we have a function f : Int -> Int, then it seems quite natural to specialize this function into a function f' : Nat -> Nat (which may make use of the fact that Nat only contains the positive elements of Int). However, according to our subtyping rule f' \not<= f, since the domain of f' is smaller than the domain of f. For an intuitive understanding of the function subtyping rule, it may be helpful to regard a function as a service. The domain of the function may then be interpreted as characterizing the restrictions imposed on the client of the service (the caller of the function) and the codomain of the function as somehow expressing the benefits for the client and the obligations for the (implementor of the) function. Now, as we have already indicated, to refine or improve on a service means to relax the restrictions imposed on the client and to strengthen the obligations of the server. This, albeit in a syntactic way, is precisely what is expressed by the contravariance rule for function subtyping.

Objects as records

Our interest in the subtype relation is primarily directed towards objects. However, since real objects involve self-reference and possibly recursively defined methods, we will first study the subtyping relation for objects as (simple) records. Our notion of objects as records is based on the views expressed in  [Ca84]. Objects may be regarded as records (where a record is understood as a finite association of values to labels), provided we allow functions to occur as the value of a record field.

Objects as records

  • record = finite association of values to labels

Field selection -- basic operation

  • (a = 3, b = true ).a == 3

Typing rule

  • \ffrac{ e_1 : %t_1 and ... and e_n : %t_n }{ { a_1 = e1,..., a_n = e_n } : { a_1 : %t_1, ..., a_n : %t_n } }
slide: The object subtype relation
 The basic operation with records is field selection which, when the value of the field accessed is a function, may be applied for method invocation. The typing rule for records follows the construction of the record: the type of a record is simply the record type composed of the types of the record's components. See slide 9-objects. In the previous section we have already characterized the subtyping relation between records. This characterization is repeated in slide 9-ex-objects. The following is meant to justify this characterization. Let us first look at a number of examples that illustrate how the subtype relation fits into the mechanism of derivation by inheritance.

Subtyping -- examples

 

  type any = { }
  type entity = { age : int }
  type vehicle = { age : int, speed : int }
  type machine = { age : int, fuel : string }
  type car = { age : int, speed : int, fuel : string }

Subtyping rules

  • %t <= %t
  • \ffrac{ %s_1 <= %t_1, ..., %s_n <= %t_n }{ { a_1 : %s_1, ..., a_{n + m} : %s_{n + m} } <= { a_1 : %t_1 , ..., a_n : %t_n } }
slide: Examples of object subtyping
 Suppose we define the type any as the record type having no fields. In our view of types as constraints, the empty record may be regarded as imposing no constraints. This is in agreement with our formal characterization of subtyping, since according to the record subtyping rule the record type any is a supertype of any other record type. Subtyping in the sense of refinement means adding constraints, that is information that constrains the set of possible elements associated with the type. The record type entity, which assumes a field age, is a subtype of any, adding the information that age is a relevant property for an entity. Following the same line of reasoning, we may regard the types vehicle and machine as subtypes of the type entity. Clearly, we may have derived the respective types by applying inheritance. For example, we may derive vehicle from entity by adding the field speed, and machine from entity by adding the field fuel. Similarly, we may apply multiple inheritance to derive the type car from vehicle and machine, where we assume that the common field age (ultimately inherited from entity) only occurs once. Obviously, the type car is a subtype of both vehicle and machine. Each of the successive types listed above adds information that constrains the possible applicability of the type as a descriptive device. The other way around, however, we may regard each object of a particular (sub)type to be an instance of its supertype simply by ignoring the information that specifically belongs to the subtype. Mathematically, we may explain this as a projection onto the fields of the supertype. Put differently, a subtype allows us to make finer distinctions. For example, from the perspective of the supertype two entities are the same whenever they have identical ages but they may be different when regarded as vehicles (by allowing different speeds).

Conformance

The importance of subtyping for practical software development comes from the conformance requirement (or substitutability property) stating that any instance of a subtype may be used when an instance of a supertype is expected. This property allows the programmer to express the functionality of a program in a maximally abstract way, while simultaneously allowing for the refinement of these abstract types needed to arrive at an acceptable implementation. For objects as records, the refinement relation concerns both attributes and functions (as members of the object record). For attributes, refinement means providing more information. Syntactically, with respect to the (signature) type of the attribute, this means a restriction of its range. In other words, the possible values an attribute may take may only be restricted. Alternatively, the refinement relation may be characterized as restricting the non-determinism contained in the specification of the supertype, by making a more specific choice. For example, if we specify the speed range of a vehicle initially as 0..300.000 then we may restrict the speed range of a car safely to 0..300 . However, to stay within the regime of subtyping we may not subsequently enlarge this range by defining a subtype racing car with a speed range of 0..400 . Intuitively, subtyping means enforcing determinism, the restriction of possible choices. Our (syntactic) characterization of the subtyping relation between object types does not yet allow for data hiding, generics or self-reference. These issues will be treated in sections existential and self-reference. However, before that, let us look at the characterization of the subtyping relation between object types as defined (for example) for the language Emerald. The characterization given in slide 9-emerald is taken from  [DT88].

Subtyping in Emerald -- S conforms to T

  • S provides at least the operations of T
  • for each operation in T, the corresponding operation in S has the same number of arguments
  • the type of the result of operations of S conform to those of the operations of T
  • the types of arguments of operations of T conform to those of the operations of S
slide: The subtype relation in Emerald
 The object subtyping relation in Emerald is characterized in terms of conformance. The rules given above specify when an object type S conforms to an object (super) type T. These rules are in agreement with the subtyping rules given previously, including the contravariance required for the argument types of operations. Taken as a guideline, the rules specify what restrictions to obey (minimally) when specifying a subtype by inheritance. However, as we will discuss in the next section, polymorphism and subtyping is not restricted to object types only. Nor are the restrictions mentioned a sufficient criterion for a semantically safe use of inheritance.

object-oriented programming

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

Flavors of polymorphism

Polymorphism is not a feature exclusive to object-oriented languages. For example the ML language is a prime example of a non object-oriented language supporting a polymorphic type system (see Milner {\it et al.}, 1990). Also, most languages, including Fortran and Pascal, support implicit conversion between integers and floats, and backwards from floats to integers, and (in Pascal) from integer subranges to integers. Polymorphism (including such conversions) is a means to relieve the programmer from the rigidity imposed by typing. Put differently, it's a way in which to increase the expressivity of the type system.

Typing -- protection against errors
  • static -- type checking at compile time
  • strong -- all expressions are type consistent

Untyped -- flexibility
  • bitstrings, sets, %l-calculus

Exceptions to monomorphic typing:
  • overloading, coercion, subranging, value-sharing (nil)
slide: The nature of types
 Typing, as we have argued before, is important as a means to protect against errors. We must distinguish between static typing (which means that type checking takes place at compile time) and strong typing (which means that each expression must be type consistent). In other words, strong typing allows illegal operations to be recognized and rejected. Object-oriented languages (such as Eiffel, and to a certain extent C++) provide strong typing which is a mixture of static typing and runtime checks to effect the dynamic binding of method invocations. See slide 9-typing. Typed languages impose rather severe constraints on the programmer. It may require considerable effort to arrive at a consistently typed system and to deal with the additional notational complexity of defining the appropriate types. In practice, many programmers and mathematicians seem to have a preference for working in an untyped formalism, like bitstrings, (untyped) sets or (untyped) lambda calculus. We may further note that languages such as Lisp, Prolog and Smalltalk are popular precisely because of the flexibility due to the absence of static type checking.

Flavors of polymorphism

  • inclusion polymorphism -- to model subtypes and inheritance
  • parametric polymorphism -- uniformly on a range of types
  • intersection types -- coherent overloading
slide: Flavors of polymorphism
 For reliable software development, working in an untyped setting is often considered as not satisfactory. However, to make typing practical, we need to relieve the typing regime by supporting well-understood exceptions to monomorphic typing, such as overloaded functions, coercion between data types and value sharing between types (as provided by a generic nil value). More importantly, however, we must provide for controlled forms of polymorphism.

In  [CW85], a distinction is made between ad hoc polymorphism (which characterizes the mechanisms mentioned as common exceptions to monomorphic typing) and universal polymorphism (which allows for theoretically well-founded means of polymorphism). Universal polymorphism may take the form of inclusion polymorphism (which is a consequence of derivation by inheritance) or parametric polymorphism (which supports generic types, as the template mechanism offered by C++). See slide 9-flavors. The term inclusion polymorphism may be understood by regarding inheritance as a means to define the properties of a (sub)type incrementally, and thus (by adding information) delimiting a subset of the elements corresponding to the supertype. When overloading is done in a systematic fashion we may speak of intersection types, which allows for polymorphism based on a finite enumeration of types. See section calculi.

Inheritance as incremental modification

The notion of inheritance as incremental modification was originally introduced in  [WZ88]. Abstractly, we may characterize derivation by inheritance in a formula as R = P + M, where R is the result obtained by modifying the parent P by (modifier) M. See slide 9-inheritance.

Inheritance -- incremental modification

  • Result = Parent + Modifier

Example: R = { a1, a2 } + { a2, a3 } = { a1, a2, a3 }

Independent attributes: M disjoint from P
Overlapping attributes: M overrules P

Dynamic binding

  • R = {...,P_i: self ! A,...} + { ...,M_j: self ! B, ... }
slide: Inheritance as incremental modification
 For example, we may define the record consisting of attributes a_1 ... a_n by adding { a_2, a_3 } to the parent { a_1, a_2 }. Clearly, we must make a distinction between independent attributes (that occur in either P or M) and overlapping attributes (that occur in both P and M and are taken to be overruled by the definition given in M). An important property of objects, not taken into account in our interpretation of object as records given before, is that objects (as supported by object-oriented languages) may be referring to themselves. For example, both in the parent and the modifier methods may be defined that refer to a variable this or self (denoting the object itself). It is important to note that the variable self is dynamically bound to the object and not (statically) to the textual module in which the variable self occurs.  [WZ88] make a distinction between attributes that are redefined in M, virtual attributes (that need to be defined in M) and recursive attributes (that are defined in P). Each of these attributes may represent methods which (implicitly) reference self. (In many object-oriented languages, the variable self or this is implicitly assumed whenever a method defined within the scope of the object is invoked.) Self-reference (implicit or explicit) underlies dynamic binding and hence is where the power of inheritance comes from. Without self-reference method calls would reduce to statically bound function invocation.

Generic abstract data types

 Our goal is to arrive at a type theory with sufficient power to define generic (polymorphic) abstract data types. In the following section, we will develop a number of type calculi (following Pierce, 1993)\index{Pierce (1993)} that enable us to define polymorphic types by employing type abstraction. Type abstraction may be used to define generic types, data hiding and (inheritance) subtypes. The idea is that we may characterize generic types by quantifying over a type variable. For example, we may define the identity function id generically as \A T. id( x:T ) = x, stating that for arbitrary type T and element x of type T, the result of applying id to x is x. Evidently this holds for any T. In a similar way, we may employ type parameters to define generic abstract data types. Further, we may improve on our notion of objects as records by defining a packaging construct that allows for data hiding by requiring merely that there exists a particular type implementing the hidden component. Also, we may characterize the (inheritance) subtyping relation in terms of bounded quantification, that is quantification over a restricted collection of types (restricted by imposing constraints with respect to the syntactic structure of the type instantiating the type parameter).

object-oriented programming

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

Type abstraction

subsections:

In this section we will study type calculi that allow us to express the various forms of polymorphism, including inclusion polymorphism (due to inheritance), parametric polymorphism (due to generics) and intersection types (due to overloading), in a syntactic way, by means of appropriate type expressions. The type calculi are based on the typed lambda calculus originally introduced in  [Ca84] to study the semantics of multiple inheritance. We will first study some simple extensions to the typed lambda calculus and then discuss examples involving universal quantification (defining parametric types), existential quantification (hiding implementation details) and bounded quantification (modeling subtypes derived by inheritance). For those not familiar with the lambda calculus, a very elementary introduction is given below. For each calculus, examples will be given to relate the insights developed to properties of the C++ type system.

The lambda calculus

 The lambda calculus provides a very concise, yet powerful formalism to reason about computational abstraction. The introduction given here has been taken from  [Barend], which is a standard reference on this subject.

Lambda calculus -- very informal

%l


  • variables, abstractor %l, punctuation (,)

Lambda terms -- $ %L $

  • x \e %L \zline{variables}
  • M \e %L => %l x. M \e %L \zline{abstraction}
  • M \e %L and N \e %L => M N \e %L \zline{application}
slide: The lambda calculus -- terms
 Syntactically, lambda terms are built from a very simple syntax, figuring variables, the abstractor %l (that is used to bind variables in an expression), and punctuation symbols. Abstractors may be used to abstract a lambda term M into a function %l x.M with parameter x. The expression %l x.M must be read as denoting the function with body M and formal parameter x. The variable x is called the bound variable, since it is bound by the abstractor %l. In addition to function abstraction, we also have (function) application, which is written as the juxtaposition of two lambda terms. See slide lambda-terms. Behaviorally, lambda terms have a number of properties, as expressed in the laws given in slide lambda-laws.

Laws
  • ( %l x.M) N = M [ x := N ] \zline{conversion}
  • M = N => MZ = NZ and ZM = ZN
  • M = N => %l x.M = %l x.N
slide: The lambda calculus -- laws
 The most important rule is the beta conversion rule, which describes in a manner of speaking how parameter passing is handled. In other words function call, that is the application (%l x.M)N , results in the function body M in which N is substituted for x. Two other laws are the so-called extensionality axioms, which express how equality of lambda terms is propagated into application and function abstraction. These laws impose constraints upon the models characterizing the meaning of lambda terms.

Substitution

  • x[x:=N] == N
  • y[x:=N] == y if x != y
  • (%l y.M)[x:=N] == %l y.(M[x:=N])
  • (M_1 M_2 ) [x:=N] == (M_1 [x:=N]) (M_2[x:=N])
slide: The lambda calculus -- substitution
 Substitution is defined by induction on the structure of lambda terms. A variable y is replaced by N (for a substitution [x:=N]) if y is x and remains y otherwise. A substitution [x:=N] performed on an abstraction %l y.M results in substituting N for x in M if x is not y. If x is identical to y, then y must first be replaced by a fresh variable (not occurring in M). A substitution performed on an application simply results in applying the substitution to both components of the application. See slide lambda-substitution. Some examples of beta conversion are given in slide lambda-examples. In the examples, for simplicity we employ ordinary arithmetical values and operators. This does not perturb the underlying %l-theory, since both values and operations may be expressed as proper %l-terms.

Examples

 

   (\%l x.x) 1 = x[x:=1] = 1
   (\%l x.x+1) 2 = (x+1)[x:=2] = 2 + 1
   (\%l x.x+y+1) 3 = (x+y+1)[x:=3] = 3+y+1
   (\%l y.(\%l x.x+y+1) 3) 4) = 
  		 ((\%l x.x+y+1) 3)[y:=4] = 3 + 4 + 1
slide: Beta conversion -- examples
 Note that the result of a substitution may still contain free variables (as in the third example) that may be bound in the surrounding environment (as in the fourth example). Lambda calculus may be used to state properties of functions (and other programming constructs) in a general way.

Properties

  • \A M (%l x.x) M = M \zline{identity}
  • \A F \E X. F X = X \zline{fixed point}

Proof: take W = %l x.F ( xx ) and X = WW, then 


  X = WW = ( \%l x.F ( xx ) ) W = F ( WW ) = FX
slide: The lambda calculus -- properties
 Consider, for example, the statement that the identity function works for each lambda term as expected. The quantification with respect to M indicates that in each possible model for the lambda calculus (that respects the extensionality axioms given above) the identity (%l x.x)M = M holds. See slide lambda-properties. As another example, consider the statement that each function F has a fixed point, that is a value X for which FX = X. The proof given above, however, does not give us any information concerning the actual contents of the fixed point, but merely proves its existence. In the following (see section self-reference) we will write \Y(F) for the fixed point of a function F. In  [Barend], an extensive account is given of how to construct mathematical models for the lambda calculus. A semantics of our type calculus may be given in terms of such models; however we will not pursue this any further here.

A simple type calculus

 In our first version of a type calculus we will restrict ourselves to a given set of basic types (indicated by the letter %r) and function types (written %s -> %t, where %s stands for the domain and %t for the range or codomain). This version of the typed lambda calculus (with subtyping) is called %l_{ <= } in  [Pierce93] from which most of the material is taken. The %l_{<=} calculus is a first order calculus, since it does not involve quantification over types. See slide 9-c-subtypes. The structure of type expressions is given by the definition 

     \%t ::= \%r | \%t_1 -> \%t_2
where we use %t as a type identifier and %r as a meta variable for basic types. The expressions of our language, that we indicate with the letter e, are similar to lambda terms, except for the typing of the abstraction variable in %l x: %t.e.

A simple type calculus -- subtypes

%l_{ <= }


  • %t ::= %r | %t_1 -> %t_2
  • e ::= x | %l x : %t . e | e_1 e_2

Type assignment

  • \ffrac{%G |- x : %s \hspace{1cm} %G |- e : %t }{ %G |- %l x : %s . e \e %s -> %t }
  • \ffrac{%G |- e_1 : %s -> %t, e_2 : %s }{ %G |- e_1 e_2 \e %t }

Refinement

  • \ffrac{ %G |- e : %s \hspace{1cm} %G |- %s <= %t}{ %G |- e : %t }
slide: The subtype calculus
 To determine whether an expression e is correctly typed (with some type expression %t) we need type assignment rules, as given above. Typing is usually based on a collection of assumptions %G, that contains the typing of expressions occurring in the expression for which we are determining the type. In the type assignment rules and the (subtyping) refinement rules, the phrase %G |- e : %t means that the expression e has type %t, under the assumption that the type assignments in %G are valid. When %G is empty, as in |- e : %t , the type assignment holds unconditionally. Occasionally, we write %G |- e \e %t instead of %G |- e : %t for readability. These two expressions have identical meaning. The premises of a type assignment rule are given above the line. The type assignment given below the line states the assignment that may be made on the basis of these premises. For example, the first type assignment rule states that, assuming %G |- x : %s (x has type %s) and %G |- e : %t (e has type %t) then %G |- %l x : %s. e \e %s -> %t, in other words the abstraction %l x:%s.e may be validly typed as %s -> %t . Similarly, the second type assignment rule states that applying a function e_1 : %s -> %t to an expression e_2 of type %s results in an (application) expression e_1 e_2 of type %t . We may assume the basic types denoted by %r to include (integer) subranges, records and variants. As a consequence, we may employ the subtyping rules given in section subtypes to determine the subtyping relation between these types. The (subtyping) refinement rule repeated here expresses the substitutability property of subtypes, which allows us to consider an expression e of type %s, with %s <= %t, as being of type %t. In slide 9-ex-subtypes, some examples are given illustrating the assignment of types to expressions. Type assignment may to a certain extent be done automatically, by type inference, as for example in ML, see  [ML90]. However, in general, typing is not decidable when we include the more powerful type expressions treated later. In those cases the programmer is required to provide sufficient type information to enable the type checker to determine the types.

Examples

  • S = %l x:Int. x + 1
    S : Int -> Int
  • twice = %l f:Int -> Int. %l y : Int . f ( f ( y ) ) twice : ( Int -> Int ) -> Int -> Int

Application
  • S 0 = 1 \e Int
  • twice ( S ) = %l x. S S x \e Int -> Int
slide: Subtypes -- examples
 When we define the successor function S as %l x : Int. x + 1 then we may type S straightforwardly as being of type Int -> Int. Similarly, we may type the (higher order) function twice as being of type (Int -> Int) -> Int -> Int. Note that the first argument to twice must be a function. Applying twice to a function argument only results in a function. When applied to S it results in a function of type Int -> Int that results in applying S twice to its (integer) argument. The subtyping rules (partly imported from section subtypes) work as expected. We may define, for example, a function + : Real \* Real -> Int as a subtype of + : Int \* Int -> Int (according to the contra-variant subtyping rule for functions).

Subtyping in C++

 Subtyping is supported in C++ only to a very limited extent. Function subtypes are completely absent. However, class subtypes due to derivation by inheritance may be employed. Also, built-in conversions are provided, some of which are in accordance with the subtyping requirements, and some of which, unfortunately, violate the subtyping requirements. Built-in conversions exist, for example, between double and int, in both ways. However, whereas the conversion from int to double is safe, the other way around may cause loss of information by truncation. The type system sketched in slide 9-c-subtypes is quite easily mapped to a C++ context. For example, we may mimic the functions S and twice as given in slide 9-ex-subtypes in C++ as: 


  int S(int x) { return x+1; }
  int twice(int f(int), int y) { return f(f(y)); }
  int twice_S(int y) { return twice(S,y); }
slide: Types in C++
 Nevertheless, the type system of C++ imposes some severe restrictions. For example, functions may not be returned as a value from functions. (Although we may provide a workaround, when we employ the operator() function for objects.) The absence of function subtyping becomes clear when, for example, we call the function twice with the function SD, which is defined as: 


  int SD(double x) { return x+1; } // twice(SD) rejected
slide: SD example
 According to the subtyping rules and in accordance with the substitutability requirement, we employ SD whenever we may employ S. But not so in C++. We run into similar limitations when we try to refine an object class descriptions following the object subtype refinement rules. 

  class P { 
   P  

  public:
  P() { _self = 0; }
  virtual P* self() {
  	return _self?_self->self():this;
  	}
  virtual void attach(C* p) {
  	_self = p;
  	}
  private:
  P* _self;
  };
  
  class C : public P { 
    C <= P  

  public:
  C() : P(this) { }
  C* self() { // ANSI/ISO
  	return _self?_self->self():this;
  	}
  void attach(P* p) {  // rejected
  	p->attach(self()); 
  	} 
  void redirect(C* c) { _self = c; }
  private:
  C* _self;
  };
slide: Subtyping in C++
 Suppose we have a parent class P which offers the member functions self and attach, as in slide 9-cc-sub. The meaning of the function self is that it de-references the _self variable if it is non-zero and delivers this otherwise. (See section hush for an example of its use.) The function attach may be used to connect an instance of C to the _self variable. The class C in its turn inherits from P and redefines self and attach. Syntactically, both refinements are allowed, due to the function subtype refinements rules. The function self is redefined to deliver a more tightly specified result, and the attach function is allowed to take a wider range of arguments. In a number of compilers for C++, both redefinitions are considered illegal. However, in the ANSI/ISO standard of C++, redefining a member function to deliver a subtype (that is, derived class) pointer will be allowed. Redefining attach, as has been done for C is probably not a wise thing to do, since it changes the semantics of attach as defined for the parent class P. In effect, it allows us to write c->attach(p) instead of p->attach(c->self()), for P\!* p and C\!* c. Nevertheless, from a type theoretical perspective, there seem to be no grounds for forbidding it.

Intersection types

We define our second version of the typed lambda calculus ( %l_{ /\ }) as an extension of the first version (%l_{ <= }), an extension which provides facilities for (ad hoc) overloading polymorphism. Our extension consists of adding a type expression \bigwedge [ %t_1,...,%t_n ] which denotes a finite conjunction of types. Such a conjunction of types, that we will also write as %t_1 /\ ... /\ %t_n is called an intersection type. The idea is that an expression e of type \bigwedge [ %t_1,...,%t_n ] is correctly typed if e : %t_i for some i in 1..n. This is expressed in the type assignment rule given in slide 9-c-intersection.

Intersection types -- overloading

%l_{ /\ }


  • %t ::= %r | %t_1 -> %t_2 | \bigwedge [ %t_1 .. %t_n ]

Type assignment

  • \ffrac{%G |- e : %t_i (i \e 1..n)}{ %G |- e : \bigwedge [ %t_1 .. %t_n ] }

Refinement

  • \ffrac{ %G |- %s <= %t_i (i \e 1..n )}{ %G |- %s <= \bigwedge [ %t_1 .. %t_n ] }
  • \bigwedge [ %t_1 .. %t_n ] <= %t_i
  • %G |- \bigwedge [ %s -> %t_1 .. %s -> %t_n ] <= %s -> \bigwedge [ %t_1 .. %t_n ]
slide: The intersection type calculus
 The subtyping rule for intersection types states that any subtype of a type occurring in the intersection type \bigwedge [ %t_1,..., %t_n ] is itself a subtype of the intersection type. In addition we have two subtyping rules without premises, the first of which says that the intersection type itself may be regarded as a subtype of any of its components. In other words, from a typing perspective an intersection type is equal (hence may be replaced by) any of its component types. Also, we may refine a function, with domain %s, which has an intersection type \bigwedge [ %t_1,..., %t_n ] as its range into an intersection type consisting of functions %s -> %t_i for i = 1..n. Intersection types allow us to express a limited form of overloading, by enumerating a finite collection of possible types. Since the collection of types comprising an intersection type is finite, we do not need a higher order calculus here, although we might have used type abstraction to characterize intersection types.

Examples
  • + : \bigwedge [ Int \* Int -> Int, Real \* Real -> Real]
  • Int -> Int <= \bigwedge [ Int -> Int, Real -> Real ]
  • Msg -> Obj1 /\ Msg -> Obj2 <= Msg -> \bigwedge [ Obj1, Obj2 ]
slide: Intersection types -- examples
 A typical example of an intersection type is presented by the addition operator, overloaded for integers and reals, which we may define as 

    + : \bigwedge [ Int \* Int -> Int, Real \* Real -> Real ]
According to our refinement rule, we may specialize an intersection type into any of its components. For example, when we have an intersection type defining a mapping for integers and a mapping for reals, we may choose the one that fits our purposes best. This example illustrates that intersection types may be an important tool for realizing optimizations that depend upon (dynamic) typing. Similarly, we may refine a generic function working on objects into a collection of (specialized) functions by dividing out the range type. See slide 9-ex-intersection. The resulting intersection type itself may subsequently be specialized into one of the component functions. In  [CGL93], a similar kind of type is used to model the overloading of methods in objects, that may but need not necessarily be related by inheritance. The idea is to regard message passing to objects as calling a polymorphic function that dispatches on its first argument. When the type of the first argument is compatible with multiple functions (which may happen for methods that are refined in the inheritance hierarchy) the most specific function component is chosen, that is the method with the minimal object type. A similar idea is encountered in CLOS, which allows for the definition of multi-methods for which dynamic dispatching takes place for all arguments. (A problem that occurs in modeling methods as overloaded functions is that the subtyping relation between methods no longer holds, due to the domain contravariance requirement. See  [CGL93] for a possible solution.)

Overloading in C++

 Although C++ does not provide support for subtyping, it does provide extensive support for function overloading. Given a collection of functions (overloading a particular function name) C++ employs a system of matches to select the function that is most appropriate for a particular call.

Overloaded function selection rules

C++


  • [1] no or unavoidable conversions -- array->pointer, T -> const T
  • [2] integral promotion -- char->int, short->int, float->double
  • [3] standard conversions -- int->double, double->int, derived* -> base*
  • [4] user-defined conversions -- constructors and operators
  • [5] ellipsis in function declaration -- ...

Multiple arguments -- intersect rule

  • better match for at least one argument and at least as good a match for every other argument
slide: Overloading in C++
 Matches may involve built-in or user-defined conversions. The general rule underlying the application of conversions is that {\em conversions that are considered less error-prone and surprising are to be preferred over the others}. This rule is reflected in the ordering of the C++ overloading selection rules depicted in slide 9-cc-over. According to the rules, the absence of conversions is to be preferred. For compatibility, with C, array to pointer conversions are applied automatically, and also T to const T conversions are considered as unproblematic. Next, we have the integral promotion rules, allowing for the conversion of char to int and short to int, for example. These conversions are also directly inherited from C, and are safe in the sense that no information loss occurs. Further, we have the standard conversions such as int to double and derived* to base*, user-defined conversions (as determined by the definition of one-argument constructors and conversion operators), and the ... ellipsis notation, which allows us to avoid type-checking in an arbitrary manner. For selecting the proper function from a collection of overloaded functions with multiple arguments, the so-called intersect rule is used, which states that the function is selected with a better match for at least one argument and at least as good a match for every other argument. In the case that no winner can be found because there are multiple candidate functions with an equally good match, the compiler issues an error, as in the example below: 


  void f(int, double);
  void f(double, int);
  
  f(1,2.0); // f(int, double);
  f(2.0,1); // f(double,int);
  f(1,1); // error: ambiguous
slide: example
 The reason that C++ employs a system of matches based on declarations and actual parameters of functions is that the graph of built-in conversions (as inherited from C) contains cycles. For example, implicit conversions exist from int to double and double to int (although in the latter case the C++ compiler gives a warning). Theoretically, however, the selection of the best function according to the subtype relation would be preferable. However, the notion of best is not unproblematic in itself. For example, consider the definition of the overloaded function f and the classes P and C in slide 9-cc-best. 


  class P;
  class C;
  
  void f(P* p) { cout << "f(P*)"; } // (1)
  void f(C* c) { cout << "f(C*)"; } // (2)
  
  class P {
  public:
  virtual void f() { cout << "P::f"; }// (3)
  };
  
  class C : public P {
  public:
  virtual void f() { cout << "C::f"; } // (4)
  };
slide: Static versus dynamic selection
 What must be considered the best function f, given a choice between (1), (2), (3) and (4)? 


  P* p = new P; // static and dynamic P*
  C* c = new C; // static and dynamic C*
  P* pc = new C; // static P*, dynamic C*
  
  f(p); // f(P*)
  f(c); // f(C*)
  f(pc); // f(P*)
  
  p->f(); // P::f
  c->f(); // C::f
  pc->f(); // C::f
In the example given above, we see that for the functions f (corresponding to (1) and (2)) the choice is determined by the static type of the argument, whereas for the member functions f (corresponding to (3) and (4)) the choice is determined by the dynamic type. We have a dilemma. When we base the choice of functions on the dynamic type of the argument, the function subtype refinement rule is violated. On the other hand, adhering to the domain contravariance property seems to lead to ignoring the potentially useful information captured by the dynamic type of the argument.

Bounded polymorphism

Our next extension, which we call F_{ <= }, involves (bounded) universal quantification. For technical reasons we need to introduce a primitive type Top, which may be considered as the supertype of all types (including itself). Also we need type abstraction variables, that we will write as %a and %b. Our notation for a universally quantified (bounded) type is \A %a <= %s . %t, which denotes the type %t with the type variable %a replaced by any subtype %s' of %s. In a number of cases, we will simply write \A %a. %t, which must be read as \A %a <= Top. %t. Recall that any type is a subtype of Top. Observe that, in contrast to %l_{ <= } and %l_{ /\ }, the calculus F_{ <= } is second order (due to the quantification over types). In addition to the (value) expressions found in the two previous calculi, F_{ <= } introduces a type abstraction expression of the form %L %a <= %t.e and a type instantiation expression of the form e[%t]. The type abstraction expression %L %a <= %t.e is used in a similar way as the function abstraction expression, although the abstraction involves types and not values. Similar to the corresponding type expression, we write %L %a.e as an abbreviation for %L %a <= Top.e . The (complementary) type instantiation statement is written as e[%t], which denotes the expression e in which the type identifier %t is substituted for the type variable bound by the first type abstractor.

Bounded polymorphism -- abstraction

F_{ <= }


  • %t ::= Top | %a | %r | %t_1 -> %t_2 | \A %a <= %t_1. %t_2
  • e ::= x | %l x:%t.e | e_1 e_2 | %L %a <= %t.e | e [ %t ]

Type assignment

  • \ffrac{%G, %a <= %s |- e : %t }{ %G |- %L %a <= %s. e \e \A %a <= %s . %t }
  • \ffrac{%G, e : \A %a <= %s . %t \hspace{1cm} %G |- %s' <= %s }{ %G |- e [ %s' ] \e %t [ %a := %s' ] }

Refinement

  • \ffrac{ %G |- %s <= %s' \hspace{1cm} %G |- %t' <= %t}{ %G |- \A %a <= %s'.%t' <= \A %a <= %s.%t }
slide: The bounded type calculus
 The type assignment rule for type abstraction states that, when we may type an expression e as being of type %t (under the assumption that %a <= %s), then we may type %L %a <= %s.e as being of type \A %a <= %s.%t. The type assignment rule for type instantiation characterizes the relation between type instantiation and substitution (which is notationally very similar). When we have an expression e of type \A %a <= %s.%t and we have that %s' <= %s, then e[%s'] is of type %t [ %a := %s' ], which is %t with %s' substituted for %a. See slide 9-c-bounded. The refinement rule for bounded types states the subtyping relation between two bounded types. We have that \A %a <= %s' . %t' is a subtype of \A %a <= %s.%t whenever %s <= %s' and %t' <= %t. Notice that the relation is contravariant with respect to the types bounding the abstraction, similar as for the domains of function subtypes in the function subtyping rule. In contrast to the polymorphism due to object type extensions and overloading, bounded polymorphism (employing type quantifiers) is an example of what we have called parametric polymorphism. In effect, this means that we must explicitly give a type parameter to instantiate an object or function of a bounded (parametric) type, similar to when we use a template in C++. The examples given in slide 9-ex-parameters illustrate how we may define and subsequently type parametric functions. In these examples, we employ the convention that in the absence of a bounding type we assume Top as an upper limit. The examples are taken from  [CW85].

Examples

  • id = %L %a. %l x:%a.x id : \A %a. %a -> %a
  • twice1 = %L %a.%l f: %L %b. %b -> %b. %l x:%a. f[%a](f[%a](x))
    twice1 : \A %a. \A %b. (%b -> %b) -> %a -> %b
  • twice2 = %L %a.%l f: %a -> %a. %l x:%a. f(f(x))
    twice2 : \A %a. (%a -> %a) -> %a -> %a

Applications
  • id [ Int ] ( 3 ) = 3
  • twice1 [ Int ] ( id )( 3 ) = 3
  • twice1 [ Int ] ( S ) = illegal
  • twice2 [ Int ] ( S )( 3 ) = 5
slide: Parametrized types -- examples
 The (generic) identity function id is defined as %L %a.%l x:%a.x, which states that when we supply a particular type, say Int, then we obtain the function %l x:Int. x. Since the actual type used to instantiate id is not important, we may type id as being of type \A %a.%a -> %a. In a similar way, we may define and type the two (generic) variants of the function twice. Notice the difference between the two definitions of twice. The first variant requires the function argument itself to be of a generic type, and fails (is incorrectly typed) for the successor function S which is (non generic) of type Int -> Int. In contrast, the second variant accepts S, and we may rely on the automatic conversion of id : \A %a. %a -> %a to id [ Int ] : Int -> Int (based on the second type assignment rule) to accept id as well. The interplay between parametric and inclusion polymorphism is illustrated in the examples presented in slide 9-ex-quantification. Recall that inclusion polymorphism is based on the subtyping relation between records (which states that refinement of a record type involves the addition of components and/or refinement of components that already belong to the super type).

Bounded quantification

  • g = %L %a <= { one : Int }. %l x: %a. (x.one)
    g : \A %a <= { one : int }. %a -> Int
  • g' = %L %b . %L %a <= { one : %b }. %l x: %a. (x.one)
    g' : \A %b . \A %a <= { one : %b }. %a -> %b
  • move = %L %a <= Point. %l p:%a. %l d : Int .(p.x := p.x + d); p
    move : \A %a <= Point. %a -> Int -> %a

Application
  • g' [ Int ][ { one:Int, two : Bool }]({ one = 3, two = true }) = 3
  • move [{ x : Int, y : Int }]( { x = 0, y = 0 } )(1) = { x = 1, y = 0 }
slide: Bounded quantification -- examples
 The first example defines a function g that works on a record with at least one component one and delivers as a result the value of the component one of the argument record. The function g' is a generalized version of g that abstracts from the particular type of the one component. Notice that both g and g' may be applied to any record that conforms to the requirement stated in the bound, such as the record { one = 3, two = true } . As another example of employing bounds to impose requirements, look at the function move that is defined for subtypes of Point (which we assume to be a record containing x and y coordinates). It expects a record (that is similar to or extends Point) and an (integer) distance, and as a result delivers the modified record.

Discussion

 Parametric polymorphism is an important means to incorporate subtyping in a coherent fashion. Apart from  [Pierce93], from which we have taken most of the material presented here, we may mention  [PA93] as a reference for further study. In  [Pierce93] a calculus F_{ /\ } is also introduced in which intersection polymorphism is expressed by means of an explicit type variable. The resulting type may be written as \A %a \e { ... }, where { ... } denotes a finite collection of types. As already mentioned, intersection types may also be used to model inclusion polymorphism (see Castagna {\it et al.}, 1993).\index{Castagna {\it et al.} (1993)} It is an interesting research issue to explore the relation between parametric polymorphism and inclusion polymorphism further along this line. However, we will not pursue this line here. Instead, in the next section we will look at another application of parametric polymorphism, namely existential types that allow us to abstract from hidden component types. This treatment is based on  [CW85]. In the last section of this chapter, we will look in more detail at the role of self-reference in defining (recursive) object types, following  [CoHC90]. We will conclude this chapter with some observations concerning the relevance of such type theories for actual programming languages. In particular, we will show that Eiffel is not type consistent.

Type abstraction in C++

 Type abstraction in C++ may occur in various guises. One important means of type abstraction is to employ what we have called polymorphic base class hierarchies. For example, the function move, which was somewhat loosely characterized in slide 9-ex-quantification, may be defined in C++ as follows: 


  Point* move(Point* p, int d); // require int Point::x
  Point* move(Point* p, int d) { p.x += d; return p; }
slide: example move
 In effect, the function move accepts a pointer to an instance of Point, or any class derived from Point, satisfying the requirement that it has a public integer data member x. Similar restrictions generally hold when instantiating a template class, but in contrast to base class subtyping requirements, these restrictions will only be verified at link time. 


  template< class T > // requires T::value()
  class P {
  public:
  P(T& r) : t(r) {}
  int operator==( P& p) {
  	return t.value() == p.t.value();
  	}
  private:
  T& t;
  };
slide: Type abstraction in C++
 Consider the template class definition given in slide 9-cc-abs. Evidently, for the comparison function to operate properly, each instantiation type substituted for the type parameter T must satisfy the requirement that it has a public member function value. 


  template< class T >
  class A { 
    A<T>   

  public: 
  virtual T value() = 0;
  };
  
  class Int : public A<int> { //    Int  <=  A<int>   
  public:
  Int(int n = 0) : _n(n) {}
  int value() { return _n; }
  private:
  int _n;
  };
slide: Type instantiation
 Such a requirement may also be expressed by defining an abstract class A defining a pure virtual member function value. See slide 9-cc-abs-2. The restrictions on instantiating P may then be stated informally as the requirement that each instantiation type T must be a subtype of A for arbitrary type X. The class Int is an example of a type complying with the implicit requirements imposed by the definition of P. An example of using P is given below 


  Int i1, i2;
  P<Int> p1(i1), p2(i2);
  if ( p1 == p2 ) cout << "OK" << endl; 
 OK
slide: Example P
 Note, however, that the derivation of A<int> is by no means necessary or in any way enforced by C++.

object-oriented programming

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

Existential types -- hiding

Existential types were introduced in  [CW85] to model aspects of data abstraction and hiding. The language introduced in  [CW85] is essentially a variant of the typed lambda calculi we have looked at previously. Our new calculus, that we call F_{ \E }, is an extension of F_{ <= } with type expressions of the form \E %a <= %s. %t (to denote existential types) and expressions of the form pack[ %a = %s in %t ] (to denote values with hidden types). Intuitively, the meaning of the expression pack[ %a = %s in %t ] is that we represent the abstract type %a occurring in the type expression %t by the actual type %s (in order to realize the value e). Following the type assignment rule, we may actually provide an instance of a subtype of the bounding type as the realization of a hidden type. See slide 9-existential.

Existential types -- hiding

F_{ \E }


  • %t ::= ... | \E %a <= %t_1. %t_2
  • e ::= ... | pack[ %a = %s in %t ]. e

Type assignment

  • \ffrac{ %G |- %s' <= %s \hspace{1cm} %G |- e : %t}{ pack[ %a = %s' in %t ].e \e \E %a <= %s. %t }

Refinement

  • \ffrac{ %G |- %s <= %s' \hspace{1cm} %G |- %t' <= %t }{ %G |- \E %a <= %s' . %t' <= \E %a <= %s. %t }
slide: The existential type calculus
 The subtyping refinement rule is similar to the refinement rule for universally quantified types. Notice also here the contravariance relation between the bounding types. More interesting is what bounding types allow us to express. (As before, we will write \E %a . %t to denote \E %a <= Top. %t.) First, existential types allow us to indicate that the realization of a particular type exists, even if we do not indicate how. The declaration e : \E %a . %t tells us that there must be some type %s such that e of type %t can be realized. Apart from claiming that a particular type exists, we may also provide information concerning its structure, while leaving its actual type undetermined.

Structure -- indeterminacy
  • Top = \E %a.%a \zline{the biggest type}
  • AnyPair = \E %a \E %b.%a \* %b \zline{any pair}
  • $(3,4):\E %a.%a {\em -- does not provide sufficient structure!}
  • $(3,4):\E %a.%a \* %a

Information hiding

  • \E %a.%a \* ( %a->Int ) \zline{object, operation}
  • x : \E %a. %a \* ( %a->Int ) \zline{ \( \leadsto \) snd ( x )( fst( x )) }
slide: Existential types -- examples
 For example, the type \E %a.%a (which may clearly be realized by any type) carries no information whatsoever, hence it may be considered to be equal to the type Top. More information, for example, is provided by the type \E %a \E %b. %a \* %b which defines the product type consisting of two (possibly distinct) types. (A product may be regarded as an unlabeled record.) The type \E %a. %a \* %a gives even more information concerning the structure of a product type, namely that the two components are of the same type. Hence, for the actual product (3,4) the latter is the best choice. See slide 9-ex-existential. Existential types may be used to impose structure on the contents of a value, while hiding its actual representation. For example, when we have a variable x of which we know that it has type \E %a. %a \* ( %a -> Int ) then we may use the second component of x to produce an integer value from its first component, by snd(x)( fst(x) ), where fst extracts the first and snd the second component of a product. Clearly, we do not need to know the actual representation type for %a. A similar idea may be employed for (labeled) records. For example, when we have a record x of type \E %a.{ val : %a, op : %a -> Int } then we may use the expression x.op(x.val) to apply the operation op to the value val. Again, no knowledge of the type of val is required in this case. However, to be able to use an element of an existential type we must provide an actual representation type, by instantiating the type parameter in a pack statement.

Abstract data types -- packages

  • x:\E %a.{ val : %a, op : %a -> Int }
  • x = pack[%a = Int in { val:%a, op:%a -> Int } ]((3,S))
  • x.op(x.val) = 4

Encapsulation

pack [ representation in interface ]( contents )


  • interface -- type \E %a. { val : %a, op : %a -> Int }
  • representation -- %a = Int \zline{(hidden data type)}
  • contents -- (3,S)
slide: Packages -- examples
 The pack statement may be regarded as an encapsulation construct, allowing us to protect the inner parts of an abstract data type. When we look more closely at the pack statement, we can see three components. First, we have an interface specification corresponding to the existential type associated with the pack expression. Secondly, we need to provide an actual representation of the hidden type, Int in the example above. And finally, we need to provide the actual contents of the structure. See slide 9-ADT. In combination with the notion of objects as records, existential types provide us with a model of abstract data types. Real objects, however, require a notion of self-reference that we have not captured yet. In the next section we will conclude our exploration of type theories by discussing the F_{%m} calculus that supports recursive (object) types and inheritance.

Hiding in C++

 Naturally, the classical way of data hiding in C++ is to employ private or protected access protection. Nevertheless, an equally important means is to employ an abstract interface class in combination with forwarding. 

  class event { 
   event  

  protected:
  event(event* x) : ev(x) {}
  public:
  int type() { return ev->type(); }
  void* rawevent() { return ev; }
  private:
  event* ev;
  };
  
  class xevent : public event { 
   X  

  public:
  int type() { return X->type(); }
  private:
  struct XEvent* X;
  };
slide: Hiding in C++
 For example, as depicted in slide 9-cc-hide, we may offer the user a class event which records information concerning events occurring in a window environment, while hiding completely the underlying implementation. The actual xevent class realizing the type event may itself need access to other structures, as for example those provided by the X window environment. Yet, the xevent class itself may remain entirely hidden from the user, since events are not something created directly (note the protected constructor) but only indirectly, generally by the system in response to some action by the user.

object-oriented programming

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

Self-reference

Recursive types are compound types in which the type itself occurs as the type of one of its components. Self-reference in objects clearly involves recursive types since the expression self denotes the object itself, and hence has the type of the object. In F_{%m}, our extension of F_{<=} taken from  [CoHC90], recursive types are written as %m %a. %t[%a], where %m is the recursion abstractor and %a a type variable. The dependence of %t on %a is made explicit by writing %t[%a]. We will use the type expressions %m %a.%t[%a] to type object specifications of the form %l(self).{ a_1 = e_1, ..., a_n = e_n } as indicated by the type assignment rule below. Object specifications may be regarded as class descriptions in C++ or Eiffel.

Self-reference -- recursive types

F_{ %m }


  • %t ::= ... | %m %a. %t [%a]
  • e ::= ... | %l( self ).{ a1 = e_1, ..., a_n = e_n }

Type assignment

  • \ffrac{ %G |- e_i : %t_i \hspace{1cm} (i = 1..n) }{ %G |- %l( self ).{ a1 = %t_1,.., a_n = %t_n } \e %m%a.{ a1:%t_1,.., a_n : %t_n }[%a] }

Refinement

  • \ffrac{ %G, %a <= %b |- %s <= %t }{ %G |- %m %a.%s[%a] <= %m %b.%t [%b] }
slide: A calculus for recursive types
 The subtype refinement rule for recursive types states that %m %a. %s [%a] <= %m %b . %t[%b] if we can prove that %s <= %t assuming that %a <= %b. An object specification %l(self).{ ... } is a function with the type of the actual object as its domain and (naturally) also as its range. For convenience we will write an object specification as %l(self).F, where F denotes the object record, and the type of an object specification as %m %a.F[%a], where F[%a] denotes the (abstract) type of the record F. To obtain from an object specification %l(self).F the object that it specifies, we need to find some type %s that types the record specification F as being of type %s precisely when we assign the expression self in F the type %s. Technically, this means that the object of type %s is a fixed point of the object specification %l(self).F(self) which is of type %s -> %s. We write this as \Y( %l(self).F(self) ) : %s, which says that the object corresponding to the object specification is of type %s. See slide 9-recursion.

Object semantics -- fixed point $ %s = F[%s] $

  • \Y ( %l( self ).F( self ) ) : %s

Unrolling -- unraveling a type

  • %m %a.F[%a] = F[ %m %a.F[%a] ]

Example

 

  T = \%m \%a.{ a:int, c:\%a, b:\%a->\%a }
  T_1 = { a:int, c:T, b:T->T, d:bool }
  T_2 = \%m \%a.{ a:int, c:\%a, b:T->T, d:bool }
  T_3 = \%m \%a.{ a:int, c:\%a, b:\%a->\%a, d:bool }

T_1, T_2 <= T, T_3 \not<= T \zline{(contravariance)}

slide: Recursive types -- examples
Finding the fixed point of a specification involves technically a procedure known as unrolling, which allows us to rewrite the type %m %a.F[%a] as F[%m %a.F[%a] ] . Notice that unrolling is valid, precisely because of the fixed point property. Namely, the object type %s is equal to %m %a.F[%a] , due to the type assignment rule, and we have that %s = F[%s] . See slide 9-ex-recursive. Unrolling allows us to reason on the level of types and to determine the subtyping relation between recursive subtypes. Consider, for example, the type declarations T and T_i (i = 1..3) above. Based on the refinement rules for object records, functions and recursive types, we may establish that T_1 <= T, T_2 <= T but T_3 \not<= T. To see that T_1 <= T, it suffices to substitute T for %a in F, where F = { a:Int, c:%a, b:%a->%a }. Since F[T] = { a:Int, c:T, b:T->T } we immediately see that T_1 only extends T with the field d:Bool, hence T_1 <= T. A similar line of reasoning is involved to determine that T_2 <= T, only we need to unroll T_2 as well. We must then establish that c:T_2 <= c:T, which follows from an application of the refinement rule. To show that T_3 \not<= T, let G[%b] = { a:Int, c:%b, b:%b->%b, d:Bool } and T_3 = %m %b.G[%b]. Then, by unrolling, T_3 = G[T_3] = { a:Int, c:T_3, b:T_3 -> T_3, d:Bool }. Now, suppose that T_3 <= T, then G[T_3] <= F[T_3] and consequently b:T_3 -> T_3 must refine b:T -> T. But from the latter requirement it follows that T_3 <= T and that T <= T_3 (by the contravariance rule for function subtyping). However, this leads to a contradiction since T is clearly not equal to T_3 because T_3 contains a field d:Bool that does not occur in T. Although analyses of this kind are to some extent satisfactory in themselves, the reader may wonder where this all leads to. In the following we will apply these techniques to show the necessity of dynamic binding and to illustrate that inheritance may easily violate the subtyping requirements.

Inheritance

In section flavors we have characterized inheritance as an incremental modification mechanism, which involves a dynamic interpretation of the expression self. In the recursive type calculus F_{%m} we may characterize this more precisely, by regarding a derived object specification C as the result of applying the modifier M to the object specification P. We employ the notation C = %l(self).P(self) \with { a_1' = e_1',...,a_k' = e_k' } to characterize derivation by inheritance, and we assume the modifier M corresponding with { a_1' = e_1', ..., a_k' = e_k' } to extend the record associated with P in the usual sense. See slide 9-self-inheritance.

Inheritance -- C = P + M

  • P = %l( self ).{ a1 = e1,...,a_n = e_n }
  • C = %l( self ).P( self ) \with \ifsli{\n}{} { a1' = e1',...,a_k' = e_k' }

Semantics -- $\Y(C) = \Y(%l( self ).M( self )(P( self )))$

  • P : %s -> %s => \Y(P):%s
  • C = %l(s).M(s)(P(s)) : %t -> %t => \Y(C):%t
slide: Inheritance semantics -- self-reference
 The meaning of an object specification C is again a fixed point \Y(C), that is \Y(%l(self).M(self)(P(self))). Now when we assume that the object specification is of type %t -> %t (and hence \Y(P) of type %t), and that C is of type %s -> %s (and hence \Y(C) of type %s), then we must require that %s <= %t to obtain a properly typed derivation. We write C <= P whenever %s <= %t. A first question that arises when we characterize inheritance as incremental modification is how we obtain the meaning of the composition of two object specifications.

Object inheritance -- dynamic binding

P = %l( self ).{ i = 5, id = self }
C = %l( self ).P( self ) \with { b = true }
\Y(P):%t where %t = %m %a.{ i:int, id:%a } and P:%t->%t

Simple typing -- \Y(C):%s = { i:int, id:%t, b:bool }
Delayed -- \Y(C):%s' = %m %a.{ i:int, id:%a, b:bool }
We have %s' <= %s \zline{(more information)}

slide: Object inheritance -- dynamic binding
Let (parent) P and (child) C be defined as above. Now, if we know that the type of \Y(P) is %t then we may simply characterize \Y(C) as being of type %s = { i:Bool, id:%t, b:Bool }. However, when we delay the typing of the P component (by first composing the record specifications before abstracting from self) then we may obtain %s' = %m %a.{ i:Int, id:%a, b:Bool } as the type of \Y(C). By employing the refinement rule and unrolling we can show that %s' <= %s. Hence, delayed typing clearly provides more information and must be considered as the best choice. Note, however, that both %s' <= %t and %s <= %t hold. See slide 9-self-dynamic. A second, important question that emerges with respect to inheritance is how self-reference affects the subtyping relation between object specifications related by inheritance. Consider the object specifications P and C given in slide 9-self-contravariance. In the (derived) specification C, the method eq is redefined to include an equality test for the b component. However, when we determine the object types corresponding to the specifications P and C we observe that C \not<= P.

Contravariance
  • P = %l( self ).{ i = 5, eq = %l(o).(o.i = self.i) }


  C = \%l( self ).P( self )  \with { b = true,
      eq = \%l(o).(o.i = self.i    and 
      o.b = self.b)
   }

\Y(P) : %t where %t = %m %a.{ i:int, eq:%a -> bool }
\Y(C):%s where %s = %m %a.{ i:int, id:%a -> bool, b: bool }
However %s \not<= %t \zline{(subtyping error)}

slide: Object inheritance -- contravariance
The reasoning is as follows. For \Y(P) : %t and \Y(C) : %s, we have that %s = %m %b.{ i:Int, id:%b -> Bool, b:Bool } which is (by unrolling) equal to { i:Int, id: %s-> Bool, b:Bool }. Now suppose that %s <= %t, then we have that { i:Int, eq:%s->Bool, b:Bool } is a subtype of { i:Int, eq:%t->Bool } which is true when eq:%s->Bool <= eq:%t->Bool and hence (by contravariance) when %s <= %t. Clearly, this is impossible. Hence %s \not<= %t. We have a problem here, since the fact that C \not<= P means that the type checker will not be able to accept the derivation of C from P, although C is clearly dependent on P. The solution to our problem lies in making the type dependency involved in deriving C from P explicit. Notice, in this respect, that in the example above we have omitted the type of the abstraction variable in the definition of eq, which would have to be written as %l x:\Y(P).x.i = self.i (and in a similar way for C ) to do it properly.

Type dependency

The expression self is essentially of a polymorphic nature. To make the dependency of object specification on self explicit, we will employ an explicit type variable similar as in F_{<=} . Let F[%a] stand for { a_1 : %t_1,...,a_n:%t } as before. We may regard F[%a] as a type function, in the sense that for some type %t the expression F[%t] results in a type. To determine the type of an object specification we must find a type %s that satisfies both %s <= F[%s] and F[%s] <= %s.

Type dependency -- is polymorphic
  • Let F[%a] = { m_1:%s_1,...,m_j:%s_j } \zline{(type function)}
  • P:\A %a <= F[%a].t -> F[%a]
  • P = %L %a <= F[%a].%l( self:%a ).{ m_1:e1,...,m_j:e_j }

F-bounded constraint %a <= F[%a]\n Object instantiation: \Y(P[%s]) for %s = %m t.F[t]\n We have P[%s]:%s -> F[%s] because F[%s] = %s

slide: Bounded type constraints
We may write an object specification as %L %a <= F[%a].%l(self:%a).{ a_1 = e_1,...,a_n = e_n }, which is typed as \A %a <= F[%a]. %a -> F[%a]. The constraint that %a <= F[%a], which is called an F-bounded constraint, requires that the subtype substituted for %a is a (structural) refinement of the record type F[%a]. As before, we have that \Y(P[%s]) = %s with %s = %m %a.F[%a], which differs from our previous definition only by making the type dependency in P explicit. See slide 9-dependency. Now, when applying this extended notion of object specification to the characterization of inheritance, we may relax our requirement that \Y(C) must be a subtype of \Y(P) into the requirement that G[%a] <= F[%a] for any %a, where F is the record specification of P and G the record specification of C.

Inheritance

 

   P = \%L \%a <= F[\%a].\%l( self: \%a).{ ... }
   C = \%L \%a <= G[\%a].\%l( self:\%a).P[\%a]( self ) \with { ... }

with recursive types
F[%a] = { i:int, id:%a -> bool }
G[%a] = { i:int, id:%a -> bool, b : bool }
Valid, because G[%a] <= F[%a]
However \Y(C[%s]) \not<=_{subtype} \Y(P[%t])

slide: Inheritance and constraints
For example, when we declare F[%a] and G[%a] as in slide 9-self-constraint, we have that G[%a] <= F[%a] for every value for %a. However, when we find types %s and %t such that \Y(C[%s]) : %s and \Y(P[%t]) : %t we (still) have that %s \not<= %t. Conclusion, inheritance allows more than subtyping. In other words, our type checker may guard the structural application of inheritance, yet will not guarantee that the resulting object types behaviorally satisfy the subtype relation.

Discussion -- Eiffel is not type consistent

 We have limited our exploration of the recursive structure of objects to (polymorphic) object variables. Self-reference, however, may also occur to class variables. The interested reader is referred to  [CoHC90]. The question that interests us more at this particular point is what benefits we may have from the techniques employed here and what lessons we may draw from applying them. One lesson, which should not come as a surprise, is that a language may allow us to write programs that are accepted by the compiler yet are behaviorally incorrect. However, if we can determine syntactically that the subtyping relations between classes is violated we may at least expect a warning from the compiler. So one benefit, possibly, is that we may improve our compilers on the basis of the type theory presented in this chapter. Another potential benefit is that we may better understand the trade-offs between the particular forms of polymorphism offered by our language of choice. The analysis given in  [CoHC90] indeed leads to a rather surprising result. Contrary to the claims made by its developer,  [CoHC90] demonstrate that Eiffel is not type consistent. The argument runs as follows. Suppose we define a class C with a method eq that takes an argument of a type similar to the type of the object itself (which may be written in Eiffel as like Current). We further assume that the class P is defined in a similar way, but with an integer field i and a method eq that tests only on i. See slide 9-self-eiffel.

Inheritance != subtyping

Eiffel 



  class C inherit P redefine eq 
  feature
    b : Boolean is true;
    eq( other : like Current ) : Boolean is
    begin
        Result := (other.i = Current.i) and
  		  (other.b = Current.b)
    end
  end C
slide: Inheritance and subtyping in Eiffel
 We may then declare variables v and p of type P. Now suppose that we have an object c of type C, then we may assign c to v and invoke the method eq for v, asking whether p is equal to v, as in 


  p,v:P, c:C 
  
  v:=c; 
  v.eq(p);   // error p has no b
slide: Example
 Since v is associated with an instance of C, but syntactically declared as being of type P, the compiler accepts the call. Nevertheless, when p is associated with an instance of P trouble will arise, since (due to dynamic binding) the method eq defined for C will be invoked while p not necessarily has a field b. When we compare the definition of C in Eiffel with how we may define C in C++, then we are immediately confronted with the restriction that we do not have such a dynamic typing mechanism as like Current in C++. Instead, we may use overloading, as shown in slide 9-self-cc. 


  class C : public P { 
   C++  

  int b;
  public:
  C() { ... }
  bool eq(C& other) { return other.i == i && other.b == b; }
  bool eq(P& other) { return other.i == i; }
  };
slide: Inheritance and subtyping in C++
 When we would have omitted the P variant of eq, the compiler complains about hiding a virtual function. However, the same problem arises when we define eq to be virtual in P, unless we take care to explicitly cast p into either a C or P reference. (Overloading is also used in  [Liskov93] to solve a similar problem.) In the case we choose for a non-virtual definition of eq, it is determined statically which variant is chosen and (obviously) no problem occurs. Considering that determining equality between two objects is somehow orthogonal to the functionality of the object proper, we may perhaps better employ externally defined overloaded functions to express relations between objects. This observation could be an argument to have overloaded functions apart from objects, not as a means to support a hybrid approach but as a means to characterize relations between objects in a type consistent (polymorphic) fashion.

object-oriented programming

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

Summary

object-oriented programming

[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources
This chapter has treated polymorphism from a foundational perspective. In section 1, we looked at abstract inheritance as employed in knowledge representation.

Abstract inheritance

1


  • 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

2

  • 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

3

  • 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

4

  • 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

5

  • 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

6

  • 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.

object-oriented programming

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

Questions

  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

object-oriented programming

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

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(s) preface I 1 2 II 3 4 III 5 6 7 IV 8 9 10 V 11 12 afterthought(s) appendix reference(s) example(s) resource(s) _

(C) Æliens 04/09/2009

You may not copy or print any of this material without explicit permission of the author or the publisher. In case of other copyright issues, contact the author.