Parametric Polymorphism in a Type-Safe, Object-Oriented Programming Language

by

Angela Marie Schuett

Thesis

Submitted in partial fulfillment of

of the requirements for the Degree of Bachelor of Arts with Honors in Computer Science

WILLIAMS COLLEGE Williamstown, Massachusetts

23 May 1994

Abstract

This thesis describes the language PolyTOIL, a type-safe, polymorphic, object-oriented programming language. PolyTOIL is an extension of the object-oriented language TOIL, also developed at Williams College. The extensions to TOIL include support for bounded and unbounded parametric polymorphism. It is relatively unusual in using a ”matching” relationship rather than subtyping to determine constraints on type arguments. Subtype polymorphism (through substitution) and inheritance are also features, though the subtype and inheritance hierarchies are not identified. A PolyTOIL interpreter has been implemented in ML and can be used to run PolyTOIL programs.

Contents

1 Introduction 1

2 The Object-Oriented Paradigm 3

3 Polymorphism 8 3.1 Implicit and Explicit Polymorphism . . . . . . . . . . . . . . . . . . . . . . 8 3.2 Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.3 Unconstrained Genericity . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.4 Constrained Genericity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

4 Syntax 16 4.1 BNF Grammar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

5 Type Checking 22 5.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 5.2 Type validity rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 5.3 Subtype rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 5.4 Matching rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 5.5 Type-checking rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

6 Natural Semantics 35 6.1 The natural semantics of PolyTOIL . . . . . . . . . . . . . . . . . . . . . . 36

7 Conclusion 41

A Using PolyTOIL 43 A.1 Using the interpreter . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 B Sample PolyTOIL programs 45

B.1 Code for Unbounded Polymorphism . . . . . . . . . . . . . . . . . . . . . . 45 B.2 Code for Bounded Polymorphism . . . . . . . . . . . . . . . . . . . . . . . . 47 B.3 Importance of matching . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

List of Figures

2.1 Classes and objects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Subtypes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 Inheritance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

3.1 Incorrect subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.2 Unconstrained genericity in C++ . . . . . . . . . . . . . . . . . . . . . . . . 12 3.3 Unbounded polymorphic function which generates a class . . . . . . . . . . 13 3.4 Bounded Polymorphic Types . . . . . . . . . . . . . . . . . . . . . . . . . . 14

4.1 Printable Bounded types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 4.2 Bounded polymorphism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

Chapter 1

Introduction

Programming languages, like spoken languages, provide a means to express thought in a precise and widely understood manner. The language used to express an idea can affect the understanding of the idea, not just by the listener, but by the speaker as well. Higher order programming languages seek to make it simpler to express certain constructs, and to guide the programmer towards a more efficient design. Some languages strive for efficiency of the computer’s time, others for efficiency of the programmer’s time in composing, and others for the simplification of the maintenance of the program. This paper describes work on PolyTOIL, a type-safe, object-oriented, programming language. The object-oriented paradigm tries to influence the programmer towards a carefully encapsulated program which is easier to write and maintain since changes to one object or capsule shouldn’t affect other objects. This is particularly useful when combined with libraries of safe, complete objects which can be used again and again by programmers. This code reuse can greatly decrease programming time.

The advantages of type-safety include: easier debugging, possible compiler optimization, and fewer run-time errors. The type of an object, at the lowest level, can describe the amount of space for storing an item of that type. A longint requires twice as much room in memory as an integer, and an array of 100 integers requires a correspondingly large amount of space. Languages which are untyped must use other means of obtaining this information, and may overestimate the amount of memory needed. At a higher level, types are useful to the programmer because they express a classification difference which exists in the data. Integers and real numbers have different properties, even outside of the computer, and if those properties are not expressed, errors can result. While it might make sense to have a height of 5.5, it really wouldn’t do to have 5.5 brothers. So, stating that a variable must be filled with a certain type can enable the compiler to find some kinds of errors, thus making the programmer’s job easier. A language is type-safe if all type errors are guaranteed to be found at compile time (as opposed to run-time). It is also important in object-oriented programming to have modular type-checking. Modular type-checking allows libraries of classes to be checked using only interface type information. This preserves encapsulation, and is important for providers of libraries who don’t wish to reveal the implementation of classes and functions. Type-safety requires static typing, that is, all variables and expressions must be bound to a type at compile time. The alternative, dynamic typing, binds some variables at run-time, and thus may allow run-time type errors. Static typing limits the expressibility of the language, but this burden can be eased through the use of polymorphism.

PolyTOIL has grown out of two other programming languages developed at Williams College: TOOPLE ([Bru93a], [BCK93]) and TOIL ([vG93], [BvG93]). TOOPLE, developed by Prof. Kim Bruce, is a functional programming language that is object-oriented and typesafe. Until TOOPLE was developed, no object-oriented languages which were proven to be type-safe existed. The work on TOOPLE shows that expressibility can be achieved by a fully type-safe language. However, because it is a functional language, TOOPLE is able to avoid some of the issues which face imperative languages. Also, programmers who are used to the imperative style have a difficult time seeing the relevance of a functional language to the issues which they face. TOIL was developed to answer this problem, and to determine whether the rules used in TOOPLE would still work with the more complicated semantics necessary for an imperative language. TOIL shares the theoretical base and philosophy of TOOPLE, but is imperative, and therefore the syntax is closer to more commonly used object-oriented languages such as Eiffel and C++.

Parametric polymorphism adds considerable power and flexibility to the existing language. Since a type-safe language is by necessity somewhat less flexible than an untyped or unsafe language, polymorphism provides a way to compensate the rigidity of static typing. TOIL features subtype polymorphism, but PolyTOIL’s bounded parametric polymorphism is based not on subtyping, but on matching. That is, the programmer specifies that the type expected must have certain methods. This is more powerful than using subtypes as the constraints because for a function (method) to be a subtype of another function, it must take parameters which are supertypes, and this is a problem when using the self-referential type, mytype. PolyTOIL’s polymorphism is more powerful than that of existing languages which base their constraints on subtyping.

In this thesis, we will specifically examine polymorphic features of PolyTOIL. The first two chapters give background information about object-oriented programming and polymorphism. Chapters 4, 5 and 6 provide a formal syntax, type-checking rules and natural semantics, respectively. All of the features of the language have been implemented. Appendix A provides instructions for using the PolyTOIL interpreter, appendix B provides code which demonstrates bounded and unbounded polymorphism.

The Object-Oriented Paradigm

Object-oriented programming has had a huge impact upon the computer industry. The principles of abstraction, encapsulation and reusability, sometimes difficult to express in other programming styles, are naturally and easily achieved within the object-oriented framework. Object-oriented programming is especially suited to very large projects, or projects which involve a team of coders. Changing the underlying representation of a queue from a linked list to an array could have catastrophic consequences in a traditional implementation, but shouldn’t cause any problems in an object-oriented program. In view of these advantages, many software vendors are switching methodologies.

An object-oriented program is based on classes, which describe variables (called instance variables), and procedures and functions (called methods) which act on those variables. A class may not be modified during run-time; it’s only purpose is to produce objects, which may be modified by sending them messages. An object is created when it is instantiated from a particular class, (think of the class as a rubber stamp, and the object as the imprint), at which time the variables specified by the class are initialized. The user/programmer then may modify the object’s variables by using the object’s methods. Only the methods provided may act upon or even view the instance variables of the object. Figure 2.1 gives an example of how classes and objects may be used in PolyTOIL. In the example, simple class has one variable, x, and one method, set. (This is not a very practical example, because, lacking a get method, the value of x can never be accessed outside of the object!) Note that inside the object, an instance variable is referenced with the word self as in self.x. An object is created from a class with the new statement. Upon creation, the instance variables are initialized, in this case, x gets the value 0. The methods may then be used to send messages to the object. The line a<=set(5) may be read as “Send the message set to the object a, with argument value 5.” The class provides a definition of the variables and methods but the object keeps track of the actual values of the variables. So, at the end of this example,

simple_class=class
  var       x=0:num
  methods   set=procedure(the_num:num)
              begin
                self.x:=the_num;
              end:proc(num);
  end;
begin
  a:=new(simple_class);
  b:=new(simple_class);
  a<=set(5);
  b<=set(6);
end.

Figure 2.1: Classes and objects

object a has x equal to 5 and object b has x equal to 6. If another set message were sent to either object, the value of x would change again in that object.

Another important feature of object-oriented languages is subtyping. Subtyping is a way to describe the relationship between the types of objects. An object type, a, is the subtype of another object type, b, if a may be used wherever b is expected. For instance, the type of the subrange of integers [5..8] is a subtype of the type of all integers, because any operation (addition, division, etc.) that can be performed on integers can be performed on the subrange without any type errors. In figure 2.1 type definitions were left out for clarity. In figure 2.2 type definitions are included in the Abbrevs section. The class type includes the types of all of the instance variables and the types of all the methods, but the object type has only the method types, because the instance variables are hidden and inaccessible from outside the object. In figure 2.2, the type of best class is a subtype of the type of basic class, because any message which could be sent to the object created from basic class can be sent to, and would be understood by, the object created from best class. Even though b is defined to be type basic type, it can hold something of type best type because best type is a subtype of basic type. Furthermore, when the message set is sent to b, x and y are both set to 4, as defined in the best class specification. To understand how this is possible, it is necessary to discuss another language feature, dynamic message dispatch. With dynamic message dispatch, each object keeps track of, and calls, only its own methods, not the methods corresponding to the type of the variable holding it.

Abbrev
basic_class_type= ClassType({x:num},{set:proc(num)});
basic_type= ObjectType{set:proc(num)};
best_class_type=
  ClassType({x:num;y:num},{set:proc(num);sum:func():num});
best_type= ObjectType{set:proc(num)};
const
basic_class=class
  var
    x:num
  methods
    set=procedure(the_num:num)
        begin
          self.x:=the_num;
        end:proc(num);
  end;
best_class=class
  var
    x:num;
    y:num;
  methods
    set=procedure(some_num:num)
        begin
          self.x:=the_num;
          self.y:=the_num;
        end:proc(num);
    sum=function():num
        begin
          return(self.x + self.y);
        end:func():num
end;
var
a:basic_type;
b:basic_type;
begin
a:=new(basic_class);
b:=new(best_class);  (*This is legal because of subtyping*)
b<=set(4);   (*This is legal because of subtyping*)
end.

Figure 2.2: Subtypes

Object-oriented languages also give the programmer the power of inheritance. Inheritance is a mechanism which allows the programmer to build upon classes which have already been defined. Using inheritance, a programmer defines a class which is the child of another class. This child class, or subclass, “inherits” all of the parent class’ instance variables and methods, and can also add its own or modify old ones. Figure 2.3 is an example of inheritance, as used in PolyTOIL.

In this example, second class has two instance variables, x and y, and two methods, set and sety. These classes can both be instantiated in the usual way, with the new statement. PolyTOIL also allows modification of instance variables and methods during inheritance. third class has two instance variables, x, which was defined in the superclass, and y, defined in the subclass. The class has one method, set, defined in the superclass, but modified in the subclass. This is much more convenient than the two separate methods, set and sety, which were required in second class. Types of objects defined through inheritance may be subtypes, as with first type and third type, but they are not necessarily subtypes. This will be examined more closely in the next chapter.

Using all of these features of object-oriented languages the programmer writes classes or groups of classes which serve as a base from which he/she can then concentrate solely on the unique facets of each problem. The base, or toolkit, might contain operations such as pretty printing, or data structures such as lists and stacks, along with their associated operations: push, pop, sort. These toolkit classes can be used over and over in many different applications, saving the programmer from having to rewrite them each time.

Abbrev
first_class_type= ClassType({x:num},{set:proc(num)});
first_type= ObjectType{set:proc(num)};
second_class_type= ClassType({x:num;y:num},{set:proc(num);sety:proc(num)});
second_type= ObjectType{set:proc(num);sety:proc(num)};
third_class_type= ClassType({x:num;y:num},{set:proc(num)});
third_type= ObjectType{set:proc(num)};
const
first_class=class
  var
    x:num
  methods
    set=procedure(the_num:num)
        begin
          self.x:=the_num;
        end:proc(num);
end;
second_class=inherit first_class
  var
    y:num
  methods
    sety=procedure(the_num:num)
        begin
          self.y:=the_num;
        end:proc(num);
end;
third_class=inherit first_class modifying set
  var
    y:num
  methods
    set=procedure(some_num:num)
        begin
          self.x:=the_num;
          self.y:=the_num;
        end:proc(num);
end;

Figure 2.3: Inheritance

Polymorphism

Polymorphism is a way of effecting code reuse by allowing greater freedom with types while still maintaining type-safety. Polymorphism allows the programmer to write objects or operations whose types are specified only generally. These objects can then be used for a variety of types, eliminating the need to write separate objects which perform the same operations on different types [CW85]. For instance, simple list structures which store integers, strings or matrices are all implemented the same way. Monomorphic languages would require three separate implementations with the only difference the type specification. Polymorphism allows a single implementation which can be used for different types of data. In this chapter we examine several different ways that various languages achieve polymorphism.

Almost every programming language has some polymorphism. For example, most languages use overloading on the common mathematical functions like +, −, ∗. Overloading occurs when one function name refers to several different functions, depending on the types of the parameters. In Pascal, the multiplication function, ∗, can be used for integers and for real numbers. However, the power to write this type of function is not given to the programmer. Overloaded functions are limited to functions provided by the language designers. These types of languages then, are not truly polymorphic, because they don’t allow the programmer to write polymorphic functions.

3.1 Implicit and Explicit Polymorphism

Some languages, notably ML and Lisp, feature implicit polymorphism [Pra84]. As the name implies, this type of polymorphism is characterized by its lack of programmer specified type parameters. In ML, type information is generally not necessary, but can be added at the programmer’s discretion. Whenever possible, type information is inferred. The type inference algorithm selects the most general typing possible. This means that all allowable polymorphism is automatically selected [Wat90]. This makes simple functions such as identity, below, infinitely reusable.

fun identity (a) = a

In this example a can have any type, so the type of identity is τ → τ, where τ is some type. The type inference algorithm can also handle more complicated cases.

fun foo (a,b) = (a+5,b)

The inferred type of foo would be int ∗ τ → int ∗ τ. That is, the parameter is a pair, where the first element, a, must be an integer, but the second element, b, can be of any type. Implicit polymorphism relieves the programmer of much of the burden of worrying about types. However, it can also cause problems by allowing types to be more general than the programmer would have intended. This can make tracking down errors much more difficult.

Explicit polymorphism requires the programmer to specify which functions will be polymorphic, and what kinds of types they can accept. Languages with this feature, also referred to as parametric polymorphism, require a type parameter. For example, in PolyTOIL, the identity function might be written as follows:

identity=function(S:atype; n:S):S
  begin
    return n;
  end: func (atype S, S):S

The first parameter, S, a type parameter, is used to specify the type of the second parameter and the return type. This function can be called with any type, but the type parameter must be passed each time, as in the following example.

answer:=identity(int,5);
answer2:=identity(horse_breed_type, Thoroughbred);

A type parameter can be filled either with one of the language defined types (int, string, boolean) or with a user defined type.

Certainly, in the identity example, parametric polymorphism is more cumbersome than implicit polymorphism. However, the overhead involved in programming with parametric polymorphism is less apparent in a larger application, such as polymorphic stacks. Parametric polymorphism is a useful addition to strongly typed languages, and because it is more specific than implicit polymorphism, it may carry corresponding rewards at debugging time.

3.2 Subtyping

Subtyping can be used to provide a form of polymorphism, because it allows types to be substituted for other types. To be a subtype, an object type must have all of the methods of the supertype, and may add methods and instance variables. In addition, subtypes may change the way methods are implemented, and may even change the type specification of the parameters of the methods, under certain circumstances. Subtyping rules are discussed in chapter 5. The possibilities for polymorphism could be illustrated in the example of a stack class which takes as a parameter a node object to be inserted. A subtype of this node object could be sent instead, because of substitutability, and a stack of the subtype objects could be created.

Subtype polymorphism is much more powerful with the use of a self-referential type. In TOIL this is “mytype”, in Eiffel, “like Current”. Programmers can use the self-referential type in the place of the object type of the object in which it appears. This allows methods to be inherited by subclasses which change the instance variables of the superclass. In the example given in figure 3.1, mytype is used in the eq method to specify that the parameter compPt be the same type as the object type.

Self-referential types also complicate the typing problem. Many object-oriented languages incorrectly conflate subtypes and subclasses, rendering their type systems unsafe. For example, in figure 3.1, ColorPoint is a subclass, but not a subtype. When the eq method is applied to FakePoint, the method that is accessed is the ColorPoint eq, not the Point eq. However, the parameter passed is of type PointType. So, the program will try to access a color from a point which has no color field. This will cause a run-time type error. Nonetheless, this code is legal in many object-oriented languages. It is legal to assign cp to FakePoint because, according to these languages, anything that is a subclass is also a subtype, so ColorPointType is a subtype of PointType. Therefore, something of type ColorPointType can be used anywhere something of type PointType is expected. It is legal to call eq with the parameter Point because FakePoint and Point are declared as type PointType. When a run-time type-error occurs in a supposedly type-safe language it is referred to as “breaking the type system”.

TOIL corrects this problem by separating the subclass and subtype rules. In TOIL, subclasses can be defined which do not generate subtypes, and subtypes need not arise from subclasses. Thus, objects with the same interface (method types), which were specified without inheritance, would still be subtypes, and substitutable. In the same way, an object which was defined through inheritance, but which made changes to the interface of its superclass, would be a legal subclass, but its type might not be a subtype, and not substitutable. This separation of the two hierarchies improves not only type-safety but expressiveness as well [Bru93b].

PointClass=class
var
x:int;
y:int;
methods
getx=...
gety=...
eq=function(compPt:mytype):bool
     begin
       return((self.x=compPt<=getx())
         && (self.y=compPt<=gety()))
     end;
ColorPointClass=inherit PointClass modifying eq;
var
color:colortype;
methods
getColor=...
eq=function(compPt:mytype):bool
     begin
       return((self.x=compPt<=getx())
         && (self.y=compPt<=gety())
         && (self.color=compPt<=getColor()))
     end;
var
Point:PointType;
FakePoint:PointType;
cp:ColorPointType;
temp:bool;
begin
Point:new(PointClass);
cp:=new(ColorPointClass);
FakePoint:=cp;
temp:=FakePoint<=eq(Point);  (*This line breaks the type-safety*)
end.

Figure 3.1: Incorrect subtyping

template<class T>
class foo {
public:
    T Identity(T* x) {return *x;}
};
foo<integer> First;
foo<string> Second;
First.Identity(int_item);
Second.Identity(string_item);

Figure 3.2: Unconstrained genericity in C++

3.3 Unconstrained Genericity

Another way to achieve polymorphism is through unconstrained genericity. This is one variety of explicit, or parametric, polymorphism. That it is unconstrained means that the function or class must work for all possible types. It must be valid for strings, integers, trees, every type. Figure 3.3 is an example of unconstrained genericity as found in C++. In this example, two different trivial objects, First and Second, are instantiated: First as an integer identity function and Second as a string identity function. In C++, templates are instantiated to objects at the time of type definition. Eiffel uses a similar mechanism to implement unconstrained genericity. In TOIL, parametric polymorphic objects can be implemented by writing a function which generates a class. In figure 3.3, the function generate test class takes a type parameter and a regular parameter. When called, it returns a class which is instantiated with the type information passed, and whose instance variable is set to the value of the parameter n. Functions which generate classes are just like regular functions in all other respects. Notice that the typing information given at the end of the function definition:

func(atype T,T):test_class_type[T]

specifies that this is a function which takes two parameters, the first a type parameter, and the second of the type specified by the first, and returns something of type test class type[T]. The class type is defined in the abbrevs section. The brackets around

abbrev  test_class_type = TFunc[T:atype T]ClassType ({value:T},
                                           {get_value:func():T});
        test_type = TFunc[T:atype T]ObjectType{get_value:func():T}
generate_test_class = function(T:atype;n:T):test_class_type[T]
         begin
            return
                class
                var
                        value=n : T
                methods
                        get_value = function():T
                          begin
                                return self.value;
                          end : func():T
                end;
        end : func(atype T,T):test_class_type[T]

var test1:test_type[num]
begin
   test1:=new(generate_test_class(num,5));
   printNum(test1<=get_value());
end.

Figure 3.3: Unbounded polymorphic function which generates a class

comparable = ObjectType({greater_than:func(comp:mytype):bool;
                            less_than:func(comp:mytype):bool;});
integer_nums = ObjectType({addition:func(addend:mytype):mytype;
                            greater_than:func(comp:mytype):bool;
                            less_than:func(comp:mytype):bool;});
names = ObjectType({greater_than:func(comp:mytype):bool;
                            less_than:func(comp:mytype):bool;
                            print:proc();});
test_class_type = TFunc[T<#comparable] ClassType ({value:T},
                        {greater_than:func(comp:mytype):bool;
                            less_than:func(comp:mytype):bool;});

Figure 3.4: Bounded Polymorphic Types

T specify that the type of test class type relies upon the value of T.

Unconstrained genericity is most useful for “container classes” such as stacks, lists, queues, because these types of classes can be used for all types of data. But, for classes which work only on a smaller set of types, more restrictions are needed for proper typechecking.

3.4 Constrained Genericity

Constrained genericity refers to that form of parametric polymorphism which is legal for a bounded set of types. One example would be a sorted list, which must contain elements that can be compared, that is, they must have ≥ or ≤ defined as functions. For example:

function return_max(f:T,s:T):T
     begin
       if f <= greater_than(s) then f
       else s;
     end;

Is only valid on the set of classes which have defined a relation greater than. Constrained genericity, or bounded polymorphism, allows the programmer to specify which operations or relations are necessary for type-safety. The programmer sets a bound on the type, usually by specifying which methods are necessary. In figure 3.4, comparable is the specification of what methods are necessary. Both integer nums and names are types which meet the specification, because they have the required methods. This bound is used in the definition of test class type, which is a polymorphic type, parameterized by T, and bounded by comparable. Notice that comparable type does not specify implementation, merely interface. A new term, matching, written <# , (written ≤_{meth} in previous TOIL papers) is needed to describe the necessary relationship between an object type and the bound it satisfies. If we have two object types, A and B, A matches B if the class from which A was created could have been defined through inheritance from the class from which B was created. The differences between matching and subtyping, and the formal rules for matching will be discussed in Chapter 5.

Constrained genericity adds considerable power to parametric polymorphism since the number of operations a programmer might want to define on completely unconstrained types is limited to simple “container classes”. Bounded polymorphism is much more expressive. It is possible to simulate constrained genericity using inheritance and unconstrained genericity, but the resulting code is very unwieldy and contrived (see [Mey88]). Nonetheless, several languages, including C++, only support unconstrained genericity.

All of the types of polymorphism discussed above are features of TOIL. Inheritance and subtyping were added by VanGent [vG93]. Parametric polymorphism, including constrained genericity, was added by the author, and will be more closely examined in the remainder of this thesis.

Syntax

The formal syntax for PolyTOIL is described on the following pages. This syntax has been written in Backus-Naur form, and accurately represents the syntax of PolyTOIL^{1}. Some notational conventions which are used in the BNF grammar are the use of all capital letters for keywords, ϵ for the empty set, and id for any non-keyword string. As an example, the rule for AbbrevDecls may be read as follows, “AbbrevDecls are either an id followed by an equal sign followed by a TypeExp followed by a semicolon followed by some more AbbrevDecls, or an id, equal sign, and a TypeExp.” So, AbbrevDecls must contain at least one element, and if more than one element exists, they are divided by semicolons.

4.1 BNF Grammar

Program ::= PROGRAM id; AbbrevList UnitBlock .

AbbrevList ::= ABBREV AbbrevDecls | ::= ϵ

AbbrevDecls ::= id = TypeExp; AbbrevDecls | ::= id = TypeExp

Block ::= :TypeExp ConstList VarList BEGIN StmtList RETURN Expr ; END

UnitBlock ::= ConstList VarList BEGIN StmtList ; END ConstList ::= CONST InitializedVarDecls |

1PolyTOIL syntax has been specified in the interpreter using sml-yacc.

::= ϵ

InitializedVarDecls ::= id = Expr : TypeExp; InitializedVarDecls | ::= id = Expr : TypeExp

VarList ::= VAR VarDecls | ::= ϵ

VarDecls ::= id : TypeExp ; VarDecls | ::= id : TypeExp | ::= id <# TypeExp ; VarDecls | ::= id <# TypeExp ; |

InitializedVarList ::= VAR InitializedVarDecls | ::= ϵ

MethodsList ::= METHODS Methods | ::= ϵ

Methods ::= id = FunctionExpr : TypeExp; Methods | ::= id = FunctionExpr : TypeExp

StmtList ::= Stmt StmtList | ::= ϵ

TypeExpList ::= NotEmptyTypeExpList | ::= ϵ

NotEmptyTypeExpList ::= TypeExp | ::= TypeExp , NotEmptyTypeExpList LabelledTypeExpList ::= { } |

::= { VarDecls }

TypeExp ::= BOOL | ::= NUM |

::= STRING |
::= MyType |
::= SelfType |

::= id | ::= id [ NotEmptyTypeExpList ] | ::= id <# TypeExp | ::= ATYPE id | ::= FUNC( TypeExpList ) : TypeExp | ::= PROC( TypeExpList ) | ::= CLASSTYPE LabelledTypeExpList , LabelledTypeExpList ) | ::= OBJECTTYPE LabelledTypeExpList | ::= TFUNC [ VarDecls ] TypeExp | ::= ( TypeExp )

Stmt ::= Expr := Expr ; | ::= WHILE Expr DO StmtList END; | ::= IF Expr THEN StmtList END; | ::= IF Expr THEN StmtList ELSE StmtList END; | ::= Expr ( ArgList ) ; |

ArgList ::= NotEmptyArgList | ::= ϵ

NotEmptyArgList ::= Expr | ::= Expr , NotEmptyArgList |

FunctionExpr ::= FUNCTION ( VarDecls ) Block |

    ::= FUNCTION () Block |

::= PROCEDURE ( VarDecls ) UnitBlock | ::= PROCEDURE () UnitBlock Idlist ::= id, Idlist |

::= ϵ

Expr ::= number |

     ::= boolean |
     ::= string |

::= id | ::= NIL |

     ::= SELF |

::= Expr ( ArgList ) |

::= Expr [ NotEmptyTypeExpList ] ( NotEmptyArgList ) |

::= ( Expr INFIXOP Expr ) |

::= Expr ⇐ id |

     ::= SELF.id |
     ::= SUPER.id |

::= FunctionExpr | ::= NEW ( Expr ) | ::= CLASS InitializedVarList MethodsList END | ::= INHERIT Expr MODIFYING Idlist SEMICOLON InitializedVarList MethodsList END | ::= INHERIT Expr SEMICOLON InitializedVarList MethodsList END

PolyTOIL also retains all of the built-in functions of TOIL, including: basic mathematical functions in an infix form (+,-,/,*,=), logical operators in infix form (&&, ||, not), and print functions (printNum, printString). It has the built-in types num (which is the same as integer in other languages), string, and boolean. In this section we will discuss the areas of syntax which affect polymorphism. For a more thorough description of the basic (non-polymorphic) syntax rules see [vG93].

The abbrev section of a PolyTOIL program allows the user to give names to types they will use later in the program. Since object and class types are commonly quite long, they are typically defined in the abbrev section. This is also the place where types which will be used as bounds are defined. Figure 4.1 shows a bound type, printable, a type that fits that bound, and the type of the class bounded by printable. The construct TFunc is used when defining the type of a parametric polymorphic function. It allows the specification of a list of type variables with their type specifications. In figure 4.1 the constraint on T is that it matches printable. If unbounded polymorphism were being specified, the type of T would be given as T:ATYPE T, which means that T may be of any type.

In order to define polymorphic functions or objects, we again use basic TOIL constructs with a few minor PolyTOIL modifications. Figure 4.1 shows a polymorphic function which

abbrev
        printable =
          ObjectType {print:proc()};
        number_class_type =
          ClassType ({me:num},{set:proc(num);print:proc()});
        number_type =
          ObjectType {set:proc(num);print:proc()};
        test_class_type =
          TFunc[T<#printable] ClassType ({value:T},
                                         {set2:proc(T);get_value:func():T});
        test_type =
          TFunc[T<#printable] ObjectType {set2:proc(T);get_value:func():T}

Figure 4.1: Printable Bounded types

generates a class. The type parameter T is bounded by printable. Notice the use of the previously defined type abbreviations. This program provides a simple, but complete, example of bounded polymorphism. The bound is provided by the definition, in the abbrevs section, of the object-type, printable, which is specified as having a method print. Number class type is the definition of the type of a class which satisfies the printable bound, and test class type is the type of a polymorphic class which uses a type variable, T, which is bounded by printable. Currently it is necessary for the programmer to write a ’Number class’, if they wish to use the properties of the built-in type num because while PolyTOIL does treat num as an object type, it does not recognize printNum as a method of a num object, but treats it as a free standing function. However, this would be an easy change to make, and hopefully future versions of PolyTOIL will make the built-in types more compatible with bounded polymorphism. Also note that type instantiations are always in square brackets, as in

test1:test_type[number_type];
test1:=new(generate_test_class[number_type](a_num));

Although PolyTOIL has some syntactic ugliness, as in the above example of the necessity of square brackets when calling a function with a type parameter, all the features are usable, and have been implemented.

generate_test_class =
  function(T<#printable; n:T):test_class_type[T]
  begin
    return
      class
      var
         value=n: T
      methods
         return_value = function():T
           begin
              self.value<=print();
              return self.value;
           end : func():T
         set = ...
   end;
end : func(T<#printable, T):test_class_type[T]
var test1:test_type[number_type];
    a_num:number_type;
    b_num:number_type
begin
   a_num:=new(number_class);
   a_num<=set(5);
   test1:=new(generate_test_class[number_type](a_num));
   b_num:=test1<=return_value();
   b_num<=print();
end.

Figure 4.2: Bounded polymorphism

Type Checking

Type checking is an important and powerful tool for debugging and compiler optimization. The importance of type-safety can be illustrated by a simple example. Imagine a program with a bug which only shows up after a set of unlikely coincidences. These types of errors are very difficult to find. Now, imagine that the program with this error is operating the space shuttle, or a nuclear weapon, or the operating system for your computer. It’s important for these programs to be error free. We may not be able to find all types of errors at compile time, but we can find all type errors, ensuring that a type error will never shut down a program written in a type-safe language. In this chapter we will examine the mechanisms and rules which make PolyTOIL a type-safe language. The syntax used in the type rules is occasionally different from the syntax of PolyTOIL. For example, in these rules, functions are all given in curried form. In addition, some types, like COMMAND, UNIT, and PROGRAM, are only used by the type system, and are not available to the programmer. Let us start with a definition of all possible type expressions.

Definition 5.0.1 Let V be an infinite collection of type variables, L be an infinite collection of labels, and C be a collection of type constants which includes at least the type constants Bool and Num. All allowable type expressions in PolyTOIL are defined as follows with respect to V and C :

1. If t ∈ V ∪ C∪ {COMMAND,UNIT,PROGRAM, ⊥, ⊤} then t is a type expression.

2. If τ is a type expression, and τ ∉ {COMMAND,UNIT, PROGRAM,⊥, ⊤} then ref τ is considered a type expression.

3. If t ∈ V then atype t is a type expression.

4. If t ∈ V and σ is a type expression then t <# σ is a type expression.

5. If σ and τ are type expressions, then so is func(σ): τ.

6. If m_{1}, …, m_{n} ∈ L and τ_{1}, …, τ_{n} are type expressions, then {m_{1}: τ_{1}; …; m_{n}: τ_{n}} is a (record) type expression.

7. Let σ and τ be record type expressions, where Mytype does not occur in σ, and Mytype ∈ V. Then the three expressions (σ, τ), ClassT ype(Mytype)(σ, τ), and ObjectT ype(Mytype)τ are type expressions. Mytype is considered to be a bound variable in the last two type expressions.

The first rule refers to the five simplest types. COMMAND is the type of an imperative command expression. For example a procedure would return type COMMAND. UNIT is a trivial type used as the parameter type for parameterless functions and procedures. PROGRAM is the type of an entire well-typed PolyTOIL program; i.e. the type returned when type-checking has successfully completed. The bottom type, ⊥, is the type of NIL. NIL is an empty object with no methods, useful because its type, ⊥, is the subtype of every object type. So, NIL may be used wherever an object is expected. The top type, ⊤, is the opposite of ⊥, in that every object type is a subtype of ⊤. It is not used by the programmer, but is important in the typing rules. The second rule simply states that the reference, or pointer, to a type is also a type. Pointers are not used in PolyTOIL by the user, but every variable is really a reference to a value. The user doesn’t need to be concerned with this, because the interpreter is able to deduce which variables are really references. The third and fourth rules concern polymorphism in PolyTOIL where atype t is the type of an unbounded type variable and t <# σ is the type of a bounded type variable. ( <# is the symbol for matching.) The fifth rule explains function types. In all of the type rules functions are in curried form. So, a function with more than one parameter would be written func(σ_{1}): (func(σ_{2}): (func(σ_{3}): τ)) It is easier to comprehend type rules written in curried form, but it is easier to program using functions with multiple parameters. So, we have chosen to express the rules in curried form but to allow the programmer to use the multiparameter form. Writing functions in that form is syntactic sugar for curried functions. Records are explained in rule six. Although PolyTOIL doesn’t have a programmer-accessible record construct (not necessary because of objects), the lists of instance variables and methods in an object are type-checked as records. The last rule describes specifically object-oriented types. ClassType(Mytype)(σ, τ) refers to the type of a class with instance variable record type σ and method record type τ. Mytype appears as a parameter to show that it is a bound variable in σ and τ. ObjectType(Mytype)τ is the type of objects and differs from ClassType in that the instance variables are hidden, so only the method record type is given. The pair type (σ, τ) represents an object type seen from inside the object. Again, σ is the type of the record of instance variables and τ is the type of the record of methods. These are all the types which are used in PolyTOIL, and in the typing and subtyping rules given in this chapter.

5.1 Definitions

Before we examine the typing, subtyping and matching rules, it is necessary to establish definitions of the symbols used in the rules. As stated earlier, <# is the symbol for matching. For subtyping, we use <: . The formal definitions of these constructs are determined by the lists of rules given in section 5.3 and section 5.4. C and E are used for determining the context of a type. The following is a formal definition of C, the type constraint system.

Definition 5.1.1 Relations of the form σ <: τ and σ <# τ, where σ and τ are type expressions, are said to be type constraints. A type constraint system is defined as follows:

1. The empty set, ϵ, is a type constraint system.

2. If C is a type constraint system, then C ∪ {τ: TYPE} is a type constraint system.

3. If C is a type constraint system, C ⊢ τ: TYPE and t <: τ is a type constraint such that the type variable t does not appear in C or τ, then C∪{t <: τ} is a type constraint system.

4. If C is a type constraint system, C ⊢ τ: TYPE, and τ is of the form ObjectT ype(Mytype)σ, and t <# τ is a type constraint such that the type variable t does not appear free in C or τ, then C ∪ {t <# τ} is a type constraint system.

So, C keeps track of the subtyping and matching relationships. A typing rule might specify that C ⊢ τ <: τ′, which can be read as: “According to the information in C, τ is a subtype of τ′.” E holds variable names and the types associated with them. It is useful for determining when a type is valid and for finding the type of an expression. The formal definition of E is as follows:

Definition 5.1.2 A type assignment E is a finite set of associations between variables and type expressions of the form x: τ, where each x is unique in E. If the relation x: τ ∈ E, then we write E(x) = τ.

5.2 Type validity rules

The following rules, necessary because of parametric polymorphism, and type parameters, determine when a type is legal, i.e. when C ⊢ τ : TYPE.

C ⊢ num: TYPE

C ⊢ bool: TYPE

C ∪ {a: TYPE} ⊢ a: TYPE

C ∪ {t <: τ} ⊢ t: TYPE

C ∪ {t <# τ} ⊢ t: TYPE

\frac{C′ = C ∪ \{t: TYPE\}, C′ ⊢ τ: TYPE}{C ⊢ (func(atype t): τ): TYPE}

\frac{C′ = C ∪ \{t: TYPE\}, C′ ⊢ τ: TYPE}{C ⊢ (func(t <# γ): τ): TYPE}

\frac{C ⊢ σ: TYPE, C ⊢ τ: TYPE}{C ⊢ (func(σ): τ): TYPE}

\frac{C ⊢ τ_{i}: TYPE where 1 ≤ i ≤ n}{C ⊢ \{m_{1}: τ_{1}; …; m_{n}: τ_{n}\}: TYPE}

\frac{C ⊢ τ: TYPE}{C ⊢ ref τ: TYPE}

\frac{C ⊢ σ: TYPE, C ⊢ τ: TYPE}{C ⊢ (σ, τ): TYPE}

\frac{C ∪ \{Mytype: TYPE\} ⊢ (σ, τ): TYPE}{C ⊢ ClassT ype(Mytype)(σ, τ): T Y P E}

\frac{C ∪ \{Mytype: TYPE\} ⊢ τ: TYPE}{C ⊢ ObjectT ype(Mytype) τ: TYPE}

\frac{f: K ⇒ K′, a: K}{f[a]: K′}

\frac{C ∪ \{t: K\} ⊢ κ: K′}{C ⊢ (TFunc[t: K]: κ): K ⇒ K′}

Most of these rules are intuitive, as in the first two, which simply specify that num and bool are always types. The other rules which have a dividing line are only slightly more complicated. The bottom expression is the expression being checked, and the top expressions specify what must be correct in order for the bottom to be a type. Let us examine the rules for checking function types.

\frac{C′ = C ∪ \{t: TYPE\}, C′ ⊢ τ: TYPE}{C ⊢ (func(atype t): τ): TYPE}

\frac{C′ = C ∪ \{t: TYPE\}, C′ ⊢ τ: TYPE}{C ⊢ (func(t <# γ): τ): TYPE}

\frac{C ⊢ σ: TYPE, C ⊢ τ: TYPE}{C ⊢ (func(σ): τ): TYPE}

The first rule states that if the parameter is a type parameter then that information is put into C, and the new C, C′, is used to check the return type, which may involve the parameter t. In this way, if τ includes t, it will check it as correct. The next rule is similar, since bounded types are also type parameters. The final rule is for normal (nontype) parameters. It specifies that the parameter and the return type must be checked for type validity.

The last two type validity rules are not TYPEing rules, but KINDing rules. In referring to a class of functions on types, we use the term kind. A kind may either be a collection of types, or a function from one kind to another kind, where the simplest kind is the kind of all types. The definition of a kind is below. Kinding enables us to describe not only functions from TYPE ⇒ TYPE, but also functions from TYPE ⇒ ( TYPE ⇒ TYPE).

5.3 Subtype rules

As was discussed in chapter one, an object is the subtype of another object if it can be used wherever the supertype object is expected. These rules specify this relationship for all of PolyTOIL’s types. Most of these rules haven’t changed since TOIL, and an explanation of them may be found in [vG93].

Refl( <: )  \frac{C ⊢ τ: TYPE}{C ⊢ τ <: τ,}

V ar( <: ) C ∪ {t <: τ} ⊢ t <: τ,

T rans( <: )  \frac{C ⊢ γ <: σ, C ⊢ σ <: τ}{C ⊢ γ <: τ} ,

Gen−Gen( <: )  \frac{C ∪ \{u: TYPE\} ⊢ τ[u/t] <: τ′[u/t′]}{C ⊢ F unc(atype t) : τ <: F unc(atype t′) : τ′} ,

where u does not occur in C, τ or τ′.

Bound−Bound( <: )\frac{C ∪ \{u <# γ\} ⊢ τ[u/t] <: τ′[u/t′]}{C ⊢ (F unc(t <# γ) : τ) <: (F unc(t <# γ) : τ′)} ,

where u does not occur in C, τ or τ′.

F unc( <: )  \frac{C ⊢ σ′ <: σ, C ⊢ τ <: τ′}{C ⊢ F unc(σ) : τ <: F unc(σ′) : τ′} ,

Rec( <: )  \frac{C ⊢ σ_{j} <: τ_{j}, for 1 ≤ j ≤ k ≤ n}{C ⊢ \{m_{1}: σ_{1}; …; m_{k}: σ_{k}; …; m_{n}: σ_{n}\} <: \{m_{1}: τ_{1}; …; m_{k}: τ_{k}\}} ,

P air( <: )  \frac{C ⊢ RecT oMem(σ) <: RecT oMem(σ′), C ⊢ τ <: τ′}{C ⊢ (σ, τ) <: (σ′, τ′)} ,

Obj( <: ),  \frac{C ∪ \{t: TYPE, s <: t\} ⊢ τ[s/Mytype] <: τ′[t/Mytype]}{C ⊢ ObjectT ype(Mytype)τ <: ObjectT ype(Mytype)τ′} .

where neither s nor t may occur free in C, τ, or τ′,

Bot( <: )  \frac{C ⊢ (ObjectT ype(Mytype)τ): TYPE}{C ⊢⊥ <: ObjectT ype(Mytype)τ} ,

T op( <: ) C ⊢ ObjectT ype(Mytype)τ <: ⊤,

First, let us examine the rules which relate to inheritance. Recall that instance variables in a class may not be modified, but instance variables in an object are modified. This is reflected in the types for objects and classes as well. The ObjectType instance variable representations are locations in memory where the values are stored. This is important in the Pair rule which examines (σ, τ), the inside type of objects. This rule uses the RecToMem function which is defined as follows: RecT oMem({v_{1}: σ_{1}; …; v_{n}: σ_{n}}) = {v_{1}: ref σ_{1}; …; v_{n}: ref σ_{n}}. Using the RecToMem function, a record of values is changed into a record of references. This allows instance variables to be checked for subtyping. Because reference types do not have nontrivial subtypes, it follows that subtypes may not change the type of any instance variable, but may only add instance variables.

We will also consider the function rules. There are three rules which address generic polymorphic type parameters, bounded polymorphic type parameters and non-type parameters. Any combination which is not addressed, for example F unc(atype t) : τ <: F unc(σ′) : τ′ can not be determined to be a subtype under our rules.

Gen−Gen( <: )  \frac{C ∪ \{u: TYPE\} ⊢ τ[u/t] <: τ′[u/t′]}{C ⊢ F unc(atype t) : τ <: F unc(atype t′) : τ′} ,

where u does not occur in τ or τ′.

To test whether two functions with unbounded polymorphic parameters have a supertypesubtype relationship, it is necessary to substitute u everywhere that t′ appears in τ′ and t appears in τ, then check τ <: τ′.

Bound−Bound( <: ) \frac{C ∪ \{u <# γ\} ⊢ τ[u/t] <: τ′[u/t′]}{C ⊢ F unc(t <# γ) : τ <: F unc(t <# γ) : τ′} ,

where u does not occur in τ or τ′.

The rule for bounded polymorphism is similar to the previous one for generics. The addition of bounds allows us to use the bound information in determining subtypes. It is not possible to determine subtyping for bounded types which have different bounds because it may not be possible to find a minimum type for the two types. The lack of a minimum type causes a failure of our type-checking algorithm.

F unc( <: ) \frac{C ⊢ σ′ <: σ, C ⊢ τ <: τ′}{C ⊢ F unc(σ) : τ <: F unc(σ′) : τ′} ,

This rule is for non-polymorphic functions. Notice that the necessary subtype relation between the parameters, σ and σ′ is the opposite of what might be expected. This is explained by thinking in terms of substitution. Consider the function f with type F unc(σ) : τ and f′ with type F unc(σ′) : τ′. The function f must be substitutable for f′ if it is a subtype. This means that a parameter of type σ′ must be valid in f, since if f was substituted for f′, this is the type of the argument that would be sent. So, σ′ must be a subtype of σ since σ′ is substituted for σ. This makes it fairly difficult to define a function which is a subtype.

5.4 Matching rules

These rules describe the matching relationship which exists between object types when the generating class of the first has inherited from the generating class of the second. However, it may also exist between classes which have no inheritance relationship. These rules are used in type-checking classes and in type-checking function application when bounded polymorphism is used.

V ar( <# ) C ∪ {t <# τ} ⊢ t <# τ,

Refl( <# )  \frac{C ⊢ ObjectT ype(Mytype)τ: TYPE}{C ⊢ ObjectT ype(Mytype)τ <# ObjectT ype(Mytype)τ,}

T rans( <# )  \frac{C ⊢ γ <# ObjectT ype(Mytype)τ, C ⊢ τ <: τ′}{C ⊢ γ <# ObjectT ype(Mytype)τ′} ,

The reason matching rules and not subtyping rules are used for bounded polymorphism is that matching provides a sufficient bound, and is much more flexible than subtyping. The major difference lies in the use of self-referential types. The subtyping rule for ObjectTypes relies on the assumption that the mytype type will be a subtype of the mytype in the supertype. However, if mytype is used as a parameter in a function, it is expected to be a supertype. Matching rules have no such requirement. The use of mytype as a parameter is especially important in programming one of the most common applications of bounded polymorphism, sorted lists. Any class with a method which checks for equality between an object and itself uses mytype. For an example of bounded polymorphic code which implements a compare method see Appendix B.3.

5.5 Type-checking rules

Finally, we come to the central set of rules. These rules make use of the subtyping, matching and typing rules which have been previously enumerated. These rules take the same form, and use the same conventions as those previous rules.

Type Assignment Rules (Program):

\frac{C_{0}, E_{0} ⊢ Block: COMMAND}{C_{0}, E_{0} ⊢ program p ; Block. : P ROGRAM}

where Block = const (constant declarations) var (variable declarations) begin (statement list) return (expression); end

Type Assignment Rules (Blocks):

ConstDecl  \frac{C, E ⊢ M: τ, C, E ∪ \{X: τ\} ⊢ rest: σ,}{C, E ⊢ const X = M; rest : σ}

V arDecl  \frac{\begin{matrix}E ⊢ τ: TYPE \\ C, E ∪ \{X: ref τ\} ⊢ rest: σ \end{matrix}}{C, E ⊢ var X: τ; rest : σ}

Block  \frac{C, E ⊢ S: COMMAND, C, E ⊢ M: σ}{C, E ⊢ begin S return M : σ; end : σ}

Type Assignment Rules (Commands):

Assn  \frac{C, E ⊢ X: ref τ, C, E ⊢ M: τ}{C, E ⊢ X: = M: COMMAND}

Cond  \frac{C, E ⊢ B: Bool, C, E ⊢ S: COMMAND, C, E ⊢ T: COMMAND}{C, E ⊢ if B then S else T end : COMMAND}
W hile  \frac{C, E ⊢ B: Bool, C, E ⊢ S: COMMAND}{C, E ⊢ while B do S end : COMMAND}
StmtList  \frac{C, E ⊢ S: COMMAND, C, E ⊢ T: COMMAND}{C, E ⊢ S; T: COMMAND}

Type Assignment Rules (Expressions): Nil C, E ⊢ NIL: ⊥

V ar C, E ⊢ X: τ, if E(X) = τ

Ref  \frac{C, E ⊢ X: ref τ}{C, E ⊢ val X: τ}
F unction  \frac{\begin{matrix}C, E′ ⊢ Block: τ \\ E ⊢ (func (σ): τ): TYPE \end{matrix}}{C, E ⊢ function (v: σ) Block: (func (σ): τ)}
where E’ = E ∪{v: σ}

UnboundF uncAppl \frac{C, E ⊢ f: func(atype σ): τ C, E ⊢ σ′: TYPE}{C, E ⊢ f(σ′): τ′}

where τ′ = τ[σ′/σ]

BoundF uncAppl \frac{\begin{matrix}C, E ⊢ f: func(σ <# γ): τ \\ C, E ⊢ σ′ <# γ \end{matrix}}{C, E ⊢ f(σ′): τ′}

where τ′ = τ[σ′/σ]

F uncAppl \frac{\begin{matrix}C, E ⊢ f: func(σ): τ \\ C, E ⊢ M: σ \end{matrix}}{C, E ⊢ f(M): τ}

Record  \frac{C, E ⊢ e_{i}: τ_{i} for all 1 ≤ i ≤ n}{C, E ⊢ \{m_{1} = e_{1}, …, m_{n} = e_{n}\}: \{m_{1}: τ_{1}; …; m_{n}: τ_{n}\}}

P roj  \frac{C, E ⊢ e: \{m_{1}: τ_{1}; …; m_{n}: τ_{n}\}}{C, E ⊢ e.m_{i}: τ_{i} for all 1 ≤ i ≤ n}

Class \frac{E ⊢ τ: TYPE C^{IV} = C ∪ \{MyT ype <# ObjectT ype τ\}, E ⊢ e_{1}: σ C^{MET H} = C^{IV} ∪ \{SelfT ype <: (RecT oMem(σ), τ)\}, E^{MET H} = E ∪ \{self : SelfT ype, close: (func(SelfT ype): MyT ype)\} ⊢ e_{2}: τ}{C, E ⊢ class(e_{1}, e_{2}): ClassT ype(σ, τ)}

Object  \frac{C, E ⊢ c: ClassT ype(σ, τ)}{C, E ⊢ new c: ObjectT ype τ}

Method  \frac{C ⊢ γ <# ObjectT ype\{m: τ\}, C, E ⊢ o: γ}{C, E ⊢ o ⇐ m: τ[γ/MyT ype]}

InstV ar  \frac{C ⊢ γ <: (\{v_{1}: σ_{1}; …; v_{n}: σ_{n}\}, τ), C, E ⊢ o: γ}{C, E ⊢ o.v_{i}: σ_{i}}

Inherits \frac{\begin{matrix}C, E ⊢ c: ClassT ype(\{v_{1}: σ_{1}; …; v_{m}: σ_{m}\}, \{m_{1}: τ_{1}; …; m_{n}: τ_{n}\}), \\ C ⊢ τ′_{1} <: τ_{1}, C^{IV} , E ⊢ a_{m+1}: σ_{m+1}, E ⊢ a′_{1}: σ_{1}, \\ C^{MET H}, E^{MET H} ⊢ e_{n+1}: τ_{n+1}, E^{MET H} ⊢ e′_{1}: τ′_{1} \end{matrix}}{\begin{matrix}C, E ⊢ inherit c modifying (\{v_{1}, m_{1}\}): \\ ClassT ype(\{v_{1}: σ_{1}; …; v_{m+1}: σ_{m+1}\}\{m_{1}: τ′_{1}; m_{2}: τ_{2}; …; m_{n+1}: τ_{n+1}\}) \end{matrix}}

where C^{IV} = C ∪ {MyT ype <# ObjectT ype {m_{1}: τ′_{1}; …; m_{n+1}: τ_{n+1}}},

C^{MET H} = C^{IV} ∪ {SelfT ype <: (RecT oMem({v_{1}: σ_{1}; …; v_{m+1}: σ_{m+1}}),

{m_{1}: τ′_{1}; …; m_{n+1}: τ_{n+1}})}
E^{MET H} = E ∪ {self : SelfT ype, close: func(SelfT ype): MyT ype,

super: SelfT ype → {m_{1}: τ_{1}; …; m_{n}: τ_{n}}} Neither MyT ype nor SelfT ype

may occur free in C or E.

Subsump  \frac{E ⊢ τ: TYPE, C ⊢ σ <: τ, C, E ⊢ e: σ}{C, E ⊢ e: τ}

The rules which are most affected by the addition of parametric polymorphism are the rules for function application, which we will examine in depth. As usual, for a more complete description of the other rules, see [vG93] or [BvG93].

UnboundF uncAppl \frac{C, E ⊢ f: func(atype σ): τ C, E ⊢ σ′: TYPE}{C, E ⊢ f(σ′): τ′}

where τ′ = τ[σ′/σ]

If the function f has type func(atype σ): τ then this rule is used. The type argument, σ′ is checked for validity, and then substituted for σ, because now that the type, σ′, is available, we no longer have to type the function with the generic type σ. It isn’t necessary to perform any other checks because the function has already been type-checked to ensure that it will be correct with any valid type as the argument.

{BoundF uncAppl \frac{\begin{matrix}C, E ⊢ f: func(σ <# γ): τ \\ C, E ⊢ σ′ <# γ \end{matrix}}{C, E ⊢ f(σ′): τ′} \atop where τ′ = τ[σ′/σ]}

If f has type func(σ <# γ): τ then this rule is used. It is the same as the rule for generics, above, except for an additional check to make sure the argument, σ′ matches the bound, γ.

F uncAppl \frac{\begin{matrix}C, E ⊢ f: func(σ): τ \\ C, E ⊢ M: σ \end{matrix}}{C, E ⊢ f(M): τ}

This rule is used for non-polymorphic functions. It merely requires that the argument M be of type σ.

Although a formal proof of type-safety does not currently exist for PolyTOIL, all the features present in TOIL have been proven to be type-safe, and the proof for PolyTOIL should follow closely.

Natural Semantics

Natural semantics are used to specify the steps taken in executing a program. They do not address type-checking at all. In the PolyTOIL interpreter, evaluation of a program occurs after type-checking, so if type errors occur, nothing is evaluated, but evaluation does not rely on any other information provided by the type-checker than the fact that it completed type-checking. Natural semantics (also referred to as operational semantics) provide a series of rules, recursively applied, specified by the expression you are starting with. The rules describe how a particular expression may be reduced, and what effects on the environment and on memory that expression has. Natural semantics are formatted similarly to typing rules in that the portion under the dividing line is the starting statement, followed by the goal, or what the starting statement will be reduced to. The ↓ can be read as ‘evaluates down to’, meaning that after other semantic rules are applied, the expression following the arrow is returned. The rules are applied until an irreducible expression is returned. In PolyTOIL, the irreducible expressions are: Numbers, Booleans, Strings, Locations (references), Functions, Records with irreducible components, Classes, and Objects. The s symbol represents the store, or the state of memory of the machine. The memory used by PolyTOIL may be thought of as an infinitely extensible one-dimensional array, referenced by numbers. New locations are accessed with the function GetNewLoc which takes a store, s, and a type t, and returns a new store, s′, and an empty location, l. The new store is the same as s, except that l is mapped to a location holding a default value of type τ. The notation used to denote placing something in a memory location is s[Loc → V]. Accessing memory is denoted by s(Loc). The store is a mapping from an integer number, the location, to the data. In order to keep track of which variables match each location, the environment, ρ is used. ρ(x) returns the location where the value of the variable x is stored. s(ρ(x)) returns the value of the variable x. To introduce a binding V for an identifier x, we use the notation ρ[V/x].

In order to understand how these concepts are used we will examine the following rules which address the evaluation of an if-then-else statement.

\frac{(B, ρ, s) ↓ (true, s′), (M, ρ, s′) ↓ (Command, s′′)}{(if B then M else N end, ρ, s) ↓ (Command, s′′)} ,

\frac{(B, ρ, s) ↓ (false, s′), (N, ρ, s′) ↓ (Command, s′′)}{(if B then M else N end, ρ, s) ↓ (Command, s′′)} ,

These rules specify that the condition of the if statement, represented by B, should be evaluated, and if it returns true, the first rule is used, otherwise the second rule is used. The environment, ρ, does not change in these rules, because PolyTOIL does not allow the definition of new variables or constants in the middle of code. The store, s does change, or rather, may change, since it is possible that the values of variables change, both in the evaluation of B, and in the evaluation of M or N.

The natural semantics for PolyTOIL are given in full here.

6.1 The natural semantics of PolyTOIL

Declarations

\frac{(e_{i}, ρ^{i}, s^{i}) ↓ (v_{i}, s^{i+1}), ρ^{i+1} = ρ^{i}[v_{i}/id_{i}], 1 ≤ i ≤ n}{(const id_{1} = e_{1}; …; id_{n} = e_{n}, ρ^{1}, s^{1}) ↓ (ρ^{n+1}, s^{n+1})} ,

\frac{(newLoc_{i}, s^{i}) = (GetNewLoc s^{i−1}), ρ^{i} = ρ^{i−1}[newLoc_{i}/id_{i}], 1 ≤ i ≤ n}{(var id_{1}: τ_{1}; …; id_{n}: τ_{n}, ρ^{0}, s^{0}) ↓ (ρ^{n}, s^{n})} ,

Blocks

\frac{(S, ρ, s) ↓ (Command, s′), (R, ρ, s′) ↓ (V, s′′)}{(begin S return R; end, ρ, s) ↓ (V, s′′)} ,

Commands

\frac{(X, ρ, s) ↓ (Loc, s′), (M, ρ, s′) ↓ (V, s′′)}{(X: = M, ρ, s) ↓ (Command, s′′[Loc ↦ V])} ,

\frac{(B, ρ, s) ↓ (true, s′), (M, ρ, s′) ↓ (Command, s′′)}{(if B then M else N end, ρ, s) ↓ (Command, s′′)} ,

\frac{(B, ρ, s) ↓ (false, s′), (N, ρ, s′) ↓ (Command, s′′)}{(if B then M else N end, ρ, s) ↓ (Command, s′′)} ,

\frac{(B, ρ, s) ↓ (true, s′), (S, ρ, s′) ↓ (Command, s′′), (while B do S end, ρ, s′′) ↓ (Command, s′′′)}{(while B do S end, ρ, s) ↓ (Command, s′′′)} ,

\frac{(B, ρ, s) ↓ (false, s′)}{(while B do S end, ρ, s) ↓ (Command, s′)} ,

\frac{(C_{1}, ρ, s) ↓ (Command, s′), (C_{2}, ρ, s′) ↓ (Command, s′′)}{(C_{1}; C_{2}, ρ, s) ↓ (Command, s′′)}

Expressions

(c, ρ, s) ↓ (c, s), where c is a constant

(x, ρ, s) ↓ (ρ(x), s), where x is a variable

\frac{(x, ρ, s) ↓ (Loc, s′), s′(Loc) = V}{(val x, ρ, s) ↓ (V, s′)} ,

(function(v: σ)B, ρ, s) ↓ (⟨function(v)B, ρ⟩, s),

\frac{\begin{matrix}(M, ρ, s^{0}) ↓ (⟨function(v: σ)B, ρ_{f}⟩, s^{1}), (N, ρ, s^{1}) ↓ (V_{1}, s^{2}), \\ (B, ρ_{f}[V_{1}/v], s^{2}) ↓ (V, s^{3}) \end{matrix}}{(M(N), ρ, s^{0}) ↓ (V, s^{3})} ,

\frac{\begin{matrix}(M, ρ, s^{0}) ↓ (⟨function(t: atype)B, ρ_{f}⟩, s^{1}), \\ (B, ρ_{f}, s^{2}) ↓ (V, s^{3}) \end{matrix}}{(M[T], ρ, s^{0}) ↓ (V, s^{3})} ,

\frac{\begin{matrix}(M, ρ, s^{0}) ↓ (⟨function(t <# γ)B, ρ_{f}⟩, s^{1}), \\ (B, ρ_{f}, s^{2}) ↓ (V, s^{3}) \end{matrix}}{(M[T], ρ, s^{0}) ↓ (V, s^{3})} ,

\frac{(e_{i}, ρ, s^{i}) ↓ (V_{i}, s^{i+1}), 1 ≤ i ≤ n}{(\{m_{1} = e_{1}: τ_{1}, …, m_{n} = e_{n}: τ_{n}\}, ρ, s^{1}) ↓ (\{m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}\}, s^{n+1})} ,

\frac{(e, ρ, s) ↓ (\{m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}\}, s′)}{(e.m_{i}, ρ, s) ↓ (V_{i}, s′)} ,

\frac{(a, ρ, s) ↓ (V_{a}, s′), (e, ρ[self /self , close/close], s′) ↓ (V_{e}, s′′)}{(class(a, e), ρ, s) ↓ (class(V_{a}, V_{e}), s′′)} ,

\frac{(a, ρ, s) ↓ (V_{a}, s′), (e, ρ[self /self , close/close], s′) ↓ (V_{e}, s′′)}{(obj(a, e), ρ, s) ↓ (obj(V_{a}, V_{e}), s′′)} ,

\frac{\begin{matrix}(c, ρ, s) ↓ (class(\{iv_{1} = V_{1}: σ_{1}, …, iv_{n} = V_{n}: σ_{n}\}, Methods), s^{0}), \\ (newLoc_{i}, s^{i}) = (GetNewLoc s^{i−1} σ_{i}), 1 ≤ i ≤ n, \\ (newLoc_{n+1}, s^{n+1}) = GetNewLoc s^{n} (σ, τ) \end{matrix}}{\begin{matrix}(new c, ρ, s) ↓ (newLoc_{n+1}, s^{i}[newLoc_{1} ↦ V_{1}, …, newLoc_{n} ↦ V_{n}, \\ newLoc_{n+1} ↦ obj(newIV, newMethods)]) \end{matrix}} ,

where newIV = {iv_{1} = newLoc_{1}: ref σ_{1}, …, iv_{n} = newLoc_{n}: ref σ_{n}}, o′ = obj(newIV, Methods), newMethods = Methods[o′/self, close_{(σ,τ)}/close,

(σ, τ)/SelfType, ObjectType τ/MyType]

\frac{\begin{matrix}(e, ρ, s) ↓ (o′, s′), \\ (newLoc, s′′) = (GetNewLoc s′(σ, τ)) \end{matrix}}{(close_{(σ,τ)} e, ρ, s) ↓ (newLoc, s′′[newLoc ↦ obj(a, newMethods)])} ,

CHAPTER 6. NATURAL SEMANTICS 39

where o′ = obj(a, Methods),

newMethods = Methods[o′/self, close_{(σ,τ)}/close,

(σ, τ)/SelfType, ObjectType τ/MyType]

\frac{(o, ρ, s) ↓ (Loc, s′), s′(Loc) = obj(a, \{m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}\})}{(o ⇐ m_{i}, ρ, s) ↓ (V_{i}, s′)} ,
\frac{(e, ρ, s) ↓ (nil, s′)}{(e ⇐ m_{i}, ρ, s) ↓ (error, s′)} ,
\frac{(o, ρ, s) ↓ (obj(\{iv_{1} = V_{1}: σ_{1}, …, iv_{n} = V_{n}: σ_{n}\}, e), s′)}{(o.iv_{i}, ρ, s) ↓ (V_{i}, s′)} ,
\frac{\begin{matrix}(P, ρ, s) ↓ (class(\{iv_{1} = V_{1}: σ_{1}, …, iv_{upd} = V_{old}: σ_{upd}, …, iv_{n} = V_{n}: σ_{n}\}, e), s′), \\ (u, ρ, s′) ↓ (V_{new}, s′′) \end{matrix}}{\begin{matrix}(inherit P modifying iv_{upd}; (\{iv_{upd} = u: σ_{upd}\}, \{\}), ρ, s) ↓ \\ (class(\{iv_{1} = V_{1}: σ_{1}, …, iv_{upd} = V_{new}: σ_{upd}, …, iv_{n} = V_{n}: σ_{n}\}, e), s′′) \end{matrix}} ,
\frac{\begin{matrix}(P, ρ, s) ↓ (class(a, \{m_{1} = V_{1}: τ_{1}, …, m_{upd} = V_{old}: τ_{upd}, …, m_{n} = V_{n}: τ_{n}\}), s′), \\ (u, ρ′, s′) ↓ (V_{new}, s′′) \end{matrix}}{\begin{matrix}(inherit P modifying m_{upd}; (\{\}, \{m_{upd} = u: τ′_{upd}\}), ρ, s) ↓ \\ (class(a, \{m_{1} = V_{1}: τ_{1}, …, m_{upd} = V_{new}: τ′_{upd}, …, m_{n} = V_{n}: τ_{n}\}), s′′) \end{matrix}} ,

where ρ′ = ρ[self /self , close/close, (function(self : SelfType).{m_{1} = V_{1}: τ_{1}, …, m_{upd} = V_{old}: τ_{upd}, …, m_{n} = V_{n}: τ_{1}})/super]

\frac{(P, ρ, s) ↓ (class(\{iv_{1} = V_{1}: σ_{1}, …, iv_{n} = V_{n}: σ_{n}\}, e), s′), (u, ρ, s′) ↓ (V_{n+1}, s′′)}{\begin{matrix}(inherit p (\{iv_{n+1} = u: σ_{n+1}\}, \{\}), ρ, s) ↓ \\ (class(\{iv_{1} = V_{1}: σ_{1}, …, iv_{n} = V_{n}: σ_{n}, iv_{n+1} = V_{n+1}: σ_{n+1}\}, e), s′′) \end{matrix}} ,
\frac{(P, ρ, s) ↓ (class(a, \{m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}\}), s′), (u, ρ′, s′) ↓ (V_{n+1}, s′′)}{\begin{matrix}(inherit p (\{\}, \{m_{n+1} = u: τ_{n+1}\}), ρ, s) ↓ \\ (class(a, \{m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}, m_{n+1} = V_{n+1}: τ_{n+1}\}), s′′) \end{matrix}} ,

where ρ′ = ρ[self /self , close/close, (function(self: SelfType).{m_{1} = V_{1}: τ_{1}, …, m_{n} = V_{n}: τ_{n}})/super]

These are all the same rules as for TOIL, except for the addition of a function application rule which can deal with types as parameters. For a full description of the intuition behind the other rules, see [vG93] and [BvG93]. Here is the original function application rule, still used for function calls which do not involve parametric polymorphism.

\frac{\begin{matrix}(M, ρ, s^{0}) ↓ (⟨function(v: σ)B, ρ_{f}⟩, s^{1}), (N, ρ, s^{1}) ↓ (V_{1}, s^{2}), \\ (B, ρ_{f}[V_{1}/v], s^{2}) ↓ (V, s^{3}) \end{matrix}}{(M(N), ρ, s^{0}) ↓ (V, s^{3})} ,

This rule specifies that the name of the function, M, be evaluated to produce the list of function parameters (v: σ), followed by the body of the function, B. Next, the argument, N, is evaluated, and the resulting value, V, is substituted into the environment for the function parameter. Finally, the body of the function is evaluated in this new environment, and the resulting value, V is returned, along with the new store, s^{3}. The new environment is not returned, thereby restoring the environment which was in place when the function was called. The new rule for polymorphic functions is very similar.

\frac{\begin{matrix}(M, ρ, s^{0}) ↓ (⟨function(t: atype)B, ρ_{f}⟩, s^{1}), \\ (B, ρ_{f}, s^{2}) ↓ (V, s^{3}) \end{matrix}}{(M[T], ρ, s^{0}) ↓ (V, s^{3})} ,

The type argument, T is necessary for type-checking, but it has no use during evaluation, so it is discarded. The body of the function is then evaluated in this environment, just as for a monomorphic function. The rule for bounded polymorphism is the same.

Conclusion

PolyTOIL is a successful marriage of several highly desirable language features. It is fully object-oriented, supporting classes, objects, methods, hidden instance variables, subclasses, subtypes, dynamic method invocation and a self-referential type, Mytype. In addition, it supports parametric polymorphism, including both unbounded and bounded quantification, with the added power and flexibility of using matching, rather than subtyping, to determine bounds. Finally, it is completely type-safe. PolyTOIL offers flexibility, expressiveness, and safety.

Several of the most popular object-oriented languages do not offer their users any typesafety. Smalltalk [GR83] is basically an untyped language. However, work is currently underway on a strongly typed version of Smalltalk called Strongtalk [BG93]. Strongtalk uses the type rules developed in TOOPLE [Bru93b] to type existing Smalltalk code. C++ [Str86], the most widely used object-oriented language, is based on the C programming language and has inherited that language’s disregard for type safety. C++ allows the programmer to make type casts and conversions, treating an integer as a pointer and so on. This makes it fairly simple to break the type system. One particularly blatant example of this is that C++ allows you to cast an object to be an integer, and then increment it, without an error! In exchange for the lack of safety, these languages offer users great flexibility. However, because PolyTOIL is not only type-safe, but modularly type-safe, library routines may be more feasible and more widely used, because they can be guaranteed to be safe without forcing the designer of the routine to reveal the actual code. Extensive use of libraries greatly ease the burden of the programmer. In addition, PolyTOIL provides unbounded and bounded polymorphism, while C++ supports only unbounded polymorphism.

Another popular object-oriented language, Eiffel, makes a much more serious effort towards type-safety. In addition, Eiffel supports the same types of polymorphism as Poly-TOIL. However, Eiffel does not separate the subclass and subtype hierarchy. As explained in section 3.2 this leads to problems when the self-referential type is used, and the type system is no longer safe. The latest version of Eiffel, Eiffel 3, corrects this problem by using a link-time checker which searches for dependencies of this type. However, this requires access to the code of libraries, and violates our modularity requirement.

A language which is somewhat similar to PolyTOIL is Emerald [BHJL86]. It features subtyping, but not classes or inheritance. However, it uses a concept similar to matching to check the applicability of operations to types. Theta, a language currently under development, shares many of the design innovations of PolyTOIL [DGLM]. Theta is being developed for use in implemented objects in the Thor object-oriented database, so it addresses issues which PolyTOIL has not been concerned with. However, Theta and PolyTOIL both share the separation of the subtype and subclass hierarchy, parametric polymorphism, and the use of matching in bounded polymorphism. Theta and PolyTOIL seem to have arrived at the same solution, coming from different starting points.

We believe that PolyTOIL offers impressive power and flexibility without compromising safety. Work is continuing on a proof of type-safety which includes the polymorphic features. Possible future work would include improvements to the interpreter, including better error messages, and support for more standard, language-defined object types. An actual compiler for the language would also be useful, and would address issues such as memory allocation which are skirted by the interpreter. In addition, an operational semantics would further establish PolyTOIL’s theoretical base. The specification of type rules and natural semantics along with the implementation show that PolyTOIL offers feasible improvements over other current object-oriented languages, but more work is needed to fully establish this language as an alternative.

Appendix A

Using PolyTOIL

An experimental interpreter for PolyTOIL has been written by Robert van Gent, with modifications and additions by the author. This interpreter contains all of the features outlined in this paper, but we have not concerned ourselves with issues of efficiency or speed. Also, error messages are rudimentary. Nonetheless, the implementation of an interpreter provides a valuable testing ground for the usefulness and practicality of language constructs.

A.1 Using the interpreter

To use the PolyTOIL interpreter on the Williams computer science network of Sun workstations, simply follow these steps:

1. Create a file, input.toil, which is either empty or which contains the input necessary for your program. This file must exist in your working directory, even if your program requires no input.

2. Type sml in bash to run Standard ML. SML is located in /usr/cs-local/sml. The PolyTOIL interpreter was written using version 0.93 of SML.

  3. Type use ``/home/cs-students/94ams/thesis/TOIL implementation/loader.sml'';

at the prompt - in sml. This loads all of the files required for the interpreter. It takes about 5 to 10 minutes to load, depending on the available memory of your machine.

  4. After the message val it = () :  unit, type eval ``a.toil''; where a.toil is

the name of your program. Even short programs may take a minute or two to run, again depending on the available memory.

5. After the program has been evaluated, results or error messages will print on the screen, ending with Exit OK. if no errors were found and execution was completed. Another program may be run simply by repeating the previous step, the whole interpreter does not have to be re-loaded each time.

Appendix B

Sample PolyTOIL programs

B.1 Code for Unbounded Polymorphism

program poly_stack;
abbrev
stack_node_class_type = TFunc[T:atype T]ClassType ({value:T;next:mytype},
                                         {get_value:func():T;
                                          get_next:func():mytype;
                                          attach_right:proc(mytype)});
stack_node_type = TFunc[T:atype T]ObjectType{get_value:func():T;
                                   get_next:func():mytype;
                                   attach_right:proc(mytype)};
stack_class_type = TFunc[S:atype S]ClassType({top:stack_node_type[S]},
                                      {push:proc(S);
                                       pop:func():S;
                                       is_empty:func():bool});
stack_type = TFunc[S:atype S]ObjectType{push:proc(S);
                                 pop:func():S;
                                 is_empty:func():bool}

const
generate_stack_node_class = function(T:atype T;n:T):stack_node_class_type[T]
  begin
    return

class
var
value=n : T;
next = nil : mytype
methods
get_value = function():T
begin
  return self.value;
end : func():T;
get_next = function():mytype
begin
  return self.next;
end : func():mytype;
attach_right =  procedure(n:mytype)
begin
  self.next:=n;
end : proc(mytype)
end;
end : func(atype T,T):stack_node_class_type[T];

stack_class = function(S:atype S):stack_class_type[S]
begin
return
class
var
top=nil : stack_node_type[S]
methods
push =  procedure(n:S)
  var
    temp:stack_node_type[S]
  begin
    temp:=self.top;
    self.top := new (generate_stack_node_class[S](n));
    self.top<=attach_right(temp);
  end : proc(S);
pop =   function():S
  var
    answer : S

begin
answer:=self.top <= get_value();
self.top := self.top<=get_next();
return answer;
end : func():S;
is_empty =      function():bool
var
answer : bool
begin
if (self.top =OBJ= nil)
then    answer:=true;
else    answer:=false;
end;
return answer;
end : func():bool
end;
end : func(atype S):stack_class_type[S]

var test1:stack_type[num];
tester:num
begin
test1:=new(stack_class[num]());
test1<=push(5);
test1<=push(4);
tester:=test1<=pop();
printNum(tester);
end.

B.2 Code for Bounded Polymorphism

program bound_test;
abbrev
printable = ObjectType {print:proc()};
number_class_type = ClassType ({me:num},{set:proc(num);print:proc()});

number_type = ObjectType {set:proc(num);print:proc()};
test_class_type = TFunc[T<#printable] ClassType ({value:T},
                                       {set2:proc(T);get_value:func():T});
test_type = TFunc[T<#printable] ObjectType {set2:proc(T);get_value:func():T}

const
number_class = class
  var
    me=0:num
  methods
    set=procedure(the_num:num)
      begin
        self.me:=the_num;
      end:proc(num);
    print=procedure()
      begin
        printNum(self.me);
      end: proc()
  end:number_class_type;
generate_test_class = function(T<#printable; n:T):test_class_type[T]
  begin
    return
      class
        var
          value=n: T
        methods
          set2=procedure(newvalue:T)
            begin
              self.value:=newvalue;
            end:proc(T);
          get_value = function():T
            begin
              self.value<=print();
              return self.value;
            end : func():T
        end;

end : func(T matches printable, T):test_class_type[T]
var test1:test_type[number_type];
a_num:number_type;
b_num:number_type
begin
a_num:=new(number_class);
a_num<=set(5);
test1:=new(generate_test_class[number_type](a_num));
b_num:=test1<=get_value();
b_num<=print();
end.

B.3 Importance of matching

program comparable;
abbrev
comparable = ObjectType{greater_than:func(mytype):bool};
integer_nums_class = ClassType({me:num},{set:proc(num);get:func():num;
                    greater_than:func(mytype):bool});
integer_nums = ObjectType{set:proc(mytype);get:func():num;
                    greater_than:func(mytype):bool};
test_class_type = TFunc[T<#comparable] ClassType ({value:T},
                {set2:proc(T);
                ig:proc(T)});
test_type = TFunc[T<#comparable] ObjectType
                {set2:proc(T);
                ig:proc(T)}
const
number_class = class
var
    me=0:num
methods
    set=procedure(the_num:num)

begin
self.me:=the_num;
end:proc(num);
get=function():num
begin
return(self.me);
end:func():num;
greater_than=function(comp:mytype):bool
begin
return(self.me>(comp<=get()));
end:func(mytype):bool
end:integer_nums_class;

generate_test_class = function(T<#comparable; n:T):test_class_type[T]
begin
return
class
var
value=n: T
methods
set2=procedure(newvalue:T)
begin
        self.value:=newvalue;
end:proc(T);
ig=procedure(comp:T)
begin
        if self.value<=greater_than(comp) then
        printNum(1);
        else
        printNum(0);
        end;
end:proc(T)
end;
end : func(T <# comparable, T):test_class_type[T]

var test1:test_type[integer_nums];
 a_num:integer_nums;
 b_num:integer_nums
begin
a_num:=new(number_class);
a_num<=set(5);
b_num:=new(number_class);
b_num<=set(6);
test1:=new(generate_test_class[integer_nums](a_num));
a_num<=ig(b_num);
end.

Bibliography

[BCK93] K. Bruce, J. Crabtree, and G. Kanapathy. An operational semantics for TOOPLE: A statically-typed object-oriented programming language. To appear in Proceedings of MFPS IX, 1993.

[BG93] Gilad Bracha and David Griswold. Strongtalk: Typechecking Smalltalk in a production environment. In Proc. ACM Symp. on Object-Oriented Programming: Systems, Languages, and Applications, pages 215–230, 1993.

[BHJL86] A. Black, N. Hutchinson, E. Jul, and H. Levy. Object structure in the Emerald system. In Proc. ACM Symp. on Object-Oriented Programming: Systems, Languages, and Applications, pages 78–86, October 1986.

[Bru93a] K. Bruce. A paradigmatic object-oriented programming language: design, static typing and semantics. Technical Report CS-92-01, revised, Williams College, 1993. To appear in Journal of Functional Programming.

[Bru93b] K. Bruce. Safe type checking in a statically typed object-oriented programming language. In Proc. ACM Symp. on Principles of Programming Languages, pages 285–298, 1993.

[BvG93] Kim B. Bruce and Robert van Gent. TOIL: A new type-safe object-oriented imperative language. Technical report, Williams College, 1993.

[CW85] L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471–522, 1985.

[DGLM] Mark Day, Robert Gruber, Barbara Liskov, and Andrew C. Myers. Abstraction mechanisms in theta. Unpublished.

[GR83] A. Goldberg and D. Robson. Smalltalk–80: The language and its implementation. Addison Wesley, 1983.

[Mey88] B. Meyer. Object-Oriented Software Construction. Prentice-Hall, 1988.

[Pra84] Terrence W. Pratt. Programming Languages. Prentice-Hall, New Jersey, 1984.

[Str86] B. Stroustrop. The C^{++} Programming Language. Addison-Wesley, 1986.

[vG93] Robert van Gent. TOIL: An imperative type-safe object-oriented language. Williams College Senior Honors Thesis, 1993.

[Wat90] David A. Watt. Programming Language Concepts and Paradigms. Prentice Hall, New York, 1990.