There are two approaches for defining subtyping relations: the syntactic and the semantic one. In the semantic approach one starts from a model of the language of interest and an interpretation of types as subsets of the model. The subtyping relation is then defined as inclusion of sets denoting types. An orthogonal issue, typical of object-oriented languages, is the issue of nominal vs. structural subtyping. We aim to integrate structural subtyping with boolean connectives and semantic subtyping for a object-oriented core language and define a Java-like programming platform that exploits the benefits of both approaches, expressible in terms of code reuse and of compactness of program writing.
A type system for a programming language is a set of deduction rules that allows to derive a type for the terms of the language. Usually, type systems are based on a subtyping relation on types. There are two approaches for defining the subtyping relation: the syntactic approach and the semantic one. The syntactic approach is more common and consists in defining the subtyping relation by means of a formal system of deductive rules. One proceeds as follows: first define the language, then the set of syntactic types and finally the subtyping relation by inference rules. In the semantic approach, instead, one starts from a model of the language and an interpretation of types as subsets of the model. The subtyping relation is then defined as inclusion of sets denoting types.
The semantic approach has received less attention than the syntactic one as it is more technical and constraining: it is not trivial to define the interpretation of the types as subsets of a model. On the other hand, it presents several advantages: for instance it allows a natural definition of boolean operators. Also the meaning of the types is more intuitive for the programmer.
The first use of the semantic approach goes back to 15 years ago, as in [
Castagna et al. in [
The semantic approach can also be applied to the calculus [
We aim at applying the semantic subtyping approach to an object-oriented core language.
Our starting point is the language Featherweight Java [
g class T riangle extends Polygon f
g class Other_Polygons extends Polygon f : : : real diagonal(Other_Polygons p) f: : :g : : : g class Rectangle extends Other_Polygons f
g class Rumble extends Other_Polygons f : : : g Another way to implement the problem is by means of an interface: public interface Diagonal f
real diagonal(Polygon p); g class Polygon f
g class T riangle extends Polygon f
g class Rectangle extends Polygon implements Diagonal f g class Rumble extends Polygon implements Diagonal f : : : g Let us now suppose that the class hierarchy has Polygon as the parent class and all other geometric figure classes that extend Polygon. Let us assume that this hierarchy is given and that it is not possible to change it afterwards. In this scenario it is more di cult to define such a method. The only way to do it in Java is by defining the method diagonal in the class Polygon and using an instanceof, for example inside a try-catch that throws an exception at run time if the argument passed to the method is a triangle.
With the use of boolean types, instead, the solution to the problem is more elegant: it is enough to define a method that has an argument of type “Polygon AND NOT Triangle” (Polygon ^ : T riangle) that permits the typechecker to control at compile time the restrictions on types. A way to implement the problem using the boolean connectives is as follows: class Polygon extends Ob ject f class Diagonal extends Ob ject f
real diagonal(Polygon ^ :T riangle p)f: : :g g At this point, it is enough to invoke the method diagonal on an argument of type Polygon: if the polygon is not a Triangle, then the method returns the length of the longest diagonal; otherwise, if the polygon is a triangle, then there will be a type error at compile time.
As an orthogonal issue, typical of object-oriented languages, is the nominal vs. structural
subtyping question. In a language where the subtyping is nominal, A is a subtype of B if
and only if it is declared to be so, that is if the class A extends (or implements) the class
(or interface) B; these relations must be declared by the programmer and are based on the
names of the classes and interfaces concerned. Recently, a new approach has emerged, the
one based on structural subtyping [
The aim of our work is to integrate structural subtyping with boolean connectives and semantic subtyping and define a Java-like programming platform that exploits the benefits of both approaches, expressible in terms of code reuse and of compactness of program writing. From the theoretical side, this calls for the definition of a set-theoretic model for the types and the study of the subtyping relation upon this model. So, algorithms for deciding the subtyping relation are needed and have to be explicitly developed. From the practical side, this calls for the development of a prototype programming environment where writing and evaluating the performances of code written in the new formalism.