A simple type calculus

Instructor's Guide

intro, inheritance, subtypes, polymorphism, types, hiding, self-reference, summary, Q/A, literature
In our first version of a type calculus we will restrict ourselves to a given set of basic types (indicated by the letter ρ) and function types (written ρ, where ρ stands for the domain and ρ for the range or codomain). This version of the typed lambda calculus (with subtyping) is called ρ in  [Pierce93] from which most of the material is taken. The λ\leqslant 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 τ:: = ρ |  τ1 → τ2 where we use τ:: = ρ |  τ1 → τ2 as a type identifier and ρ 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 ρ.
  
  
  
slide: The subtype calculus
 To determine whether an expression e is correctly typed (with some type expression τ) we need type assignment rules, as given above. Typing is usually based on a collection of assumptions τ, 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 Γ\vdash e : τ means that the expression e has type Γ\vdash e : τ, under the assumption that the type assignments in Γ are valid. When Γ is empty, as in Γ, the type assignment holds unconditionally. Occasionally, we write Γ instead of Γ 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 Γ (x has type σ) and σ (e has type τ) then Γ\vdash λx : σ. e   ∈  σ→ τ, in other words the abstraction Γ\vdash λx : σ. e   ∈  σ→ τ may be validly typed as σ→ τ. Similarly, the second type assignment rule states that applying a function σ→ τ to an expression σ→ τ of type σ→ τ results in an (application) expression σ→ τ of type σ→ τ. We may assume the basic types denoted by ρ 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 ρ, with σ\leqslant τ, as being of type σ\leqslant τ. 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.
  
  
slide: Subtypes -- examples
 When we define the successor function S as λx : Int. x + 1 then we may type S straightforwardly as being of type λx : Int. x + 1. 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 Int → 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; }
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.