1 Introduction

There are two approaches to defining subtyping relations: the syntactic and the semantic approach. Syntactic subtyping [20] is more mainstream in programming languages and is defined by means of a set of formal deductive subtyping rules. Semantic subtyping [1, 10] is more recent and less known: one defines a formal model of the language and an interpretation of types as subsets of this model. Then, subtyping is defined as set inclusion of subsets denoting types.

Orthogonally, for object-oriented languages there are two approaches to defining subtyping relations: the nominal and the structural approach [21, 22]. Nominal subtyping is based on declarations by the developer and is name-based: “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”. Structural subtyping instead is based on the structure of a class, its fields and methods: “a class A is a subtype of a class B if and only if the fields and methods of A are a superset of the fields and methods of B, and their types in A are subtypes of the types in B”. For example, the set of inhabitants of a class Student is smaller than the set of inhabitants of a class Person, as each Student is a Person, but not the other way around. However, the set of fields and methods of Student is a superset of that of Person. Hence, Student is a structural subtype of Person, even if it is not declared so.

Dardha et al. [11, 12] define boolean types—based on set-theoretic operations such as and, not, or—and semantic subtyping for Featherweight Java (FJ) [17]. This approach allows for the integration of both nominal and structural subtyping in FJ, bringing in higher guarantees of program correctness, flexibility and compactness in program writing. Unfortunately, these benefits were only presented at a theoretical level and not exploited practically, due to the lack of an implementation of the language, its types and type system.

In this paper, we present SFJ—Semantic Featherweight Java Sect. 3, an implementation of FJ with boolean types and semantic subtyping. In SFJ the developer has a larger and more expressive set of types, by using boolean connectives and, not, or, with the expected set-theoretic interpretation. On the other hand, this added expressivity does not add complexity. Rather the opposite is true, as the developer has an easier, more compact and elegant way of programming. SFJ integrates both structural and nominal subtyping, and the developer can choose which one to use. Finally, as discussed in Dardha et al. [12, Sect. 8.4], thanks to semantic subtyping, we can easily encode in SFJ standard programming constructs and features of the full Java language, such as lists, or overloading classes via multimethods [5], which are missing in FJ, thus making SFJ a more complete language closer to Java.

Example 1

(Polygons). This will be our running example both in the paper and in the tool video [27] to illustrate the benefits of boolean types and semantic subtyping developed by Dardha et al. [11, 12] and implemented as SFJ.

Consider the set of polygons, such as triangles, squares and rhombuses given by a class hierarchy. We want to define a method diagonal that takes a polygon and returns the length of its longest diagonal. This method makes sense only if the polygon passed to it has at least four sides, hence triangles are excluded. In Java this could be implemented in the following ways:

Or by means of an interface Diagonal:

Now, suppose our class hierarchy is such that Polygon is the parent class and all other geometric figures extend Polygon, which is how one would naturally define the set of polygons. Suppose the class hierarchy is given and is part of legacy code, which cannot be changed. Then again, a natural way to implement this in Java is by defining the method diagonal in the class Polygon and using an instanceof, for example, inside a try-catch construct. Then, an exception would be thrown at run time, if the argument passed to the method is a triangle.

We propose a more elegant solution, by combining boolean types and semantic subtyping, where only static type-checking is required and we implement this in SFJ [27]: it is enough to define a method diagonal that has an argument of type Polygon and not Triangle, thus allowing the type-checker to check at compile time the restrictions on types:

We can now call diagonal on an argument of type Polygon: if the polygon is not a Triangle, then the method computes and returns the length of its longest diagonal; otherwise, there will be a type error at compile time.

Structure of the Paper: In Sect. 2 we present the types and terms of the SFJ language. In Sect. 3 we present the design and implementation of SFJ; we discuss our two main algorithms, Algorithm 1 in Sect. 3.1 which checks the validity of type definitions, and Algorithm 2 in Sect. 3.2 which generates the semantic subtyping relation. Further, we discuss typing of SFJ in Sect. 3.3; nominal vs. structural subtyping in Sect. 3.5; method types in Sect. 3.6; and code generation in Sect. 3.7. We discuss related work and conclude the paper in Sect. 4.

2 Background

The technical developments behind semantic subtyping and its properties are complex, however, they are completely transparent to the programmer. The framework is detailed and proved correct in the relevant work by Dardha et al. [11, 12], and SFJ builds on that framework.

In this section we will briefly detail the types and terms of SFJ.

2.1 Types

The syntax of types \(\tau \) is defined by the following grammar:

figure a

The \(\alpha \)-types are used to type fields and the \(\mu \)-types are used to type methods. Type \(\mathbf {0}\) is the empty type. Type \({\mathbb B}\) denotes the basic types, such as integers, booleans, etc. Record types \([\widetilde{l:\tau }]\), where \(\widetilde{l}\) is a sequence of disjoint labels, are used to type objects. Arrow types \(\alpha \rightarrow \alpha \) are used to type methods.

The boolean connectives \(\mathbf {and}\) and \(\mathbf {not}\) in the \(\alpha \)-types and \(\mu \)-types have their expected set-theoretic meanings. We let \(\alpha \ \pmb {\backslash }\ \alpha '\) denote \(\alpha \ \mathbf {and}\ (\mathbf {not}\ \alpha ')\), and \(\alpha \ \mathbf {or}\ \alpha '\) denote \(\mathbf {not}(\mathbf {not}\ \alpha \ \mathbf {and}\ (\mathbf {not}\ \alpha '))\).

2.2 Terms

The syntax of terms is defined by the following grammar and is based on the standard syntax of terms in FJ [17]:

$$\begin{aligned}&{\textit{Class declaration}}&L \; {::}\!= \;&\mathbf {class} \ C \ \mathbf {extends }\ C\ \{\widetilde{\alpha \ a};\ K; \ \widetilde{M}\ \} \\&{\textit{Constructor}}&K \;{::}\!=\;&C\ (\widetilde{\alpha \ x})\ \{\ \mathbf {super}(\widetilde{x});\ \widetilde{\mathbf {this}.a}=\widetilde{x}; \} \\&{\textit{Method declaration}}&M \; {::}\!= \;&\alpha \ m\ (\alpha \ x)\ \{\ \mathbf {return}\ e; \} \\&{\textit{Expressions}}&e \; {::}\!=\;&x\ |\ c\ |\ e.a\ |\ e.m(e) \ | \ \mathbf {new}\ C(\widetilde{e}) \end{aligned}$$

We assume an infinite set of names, with some special names: \( Object \) denotes the root class, \(\mathbf {this}\) denotes the current object and \(\mathbf {super}\) denotes the parent object. We let \(A, B,\ldots \) range over classes; \(a, b,\ldots \) over fields; \(m, n,\ldots \) over methods and \(x, y, z, \ldots \) over variables.

A program \((\widetilde{L}, e)\) is a pair of a sequence of class declarations \(\widetilde{L}\), giving rise to a class hierarchy as specified by the inheritance relation, and an expression e to be evaluated. A class declaration L specifies the name of the class, the name of the parent class it extends, its typed fields, the constructor K and its method declarations M. The constructor K initialises the fields of the object by assigning values to the fields inherited by the super-class and to the fields declared in the current this class. A method declaration M specifies the signature of the method, namely the return type, the method name and the formal parameter as well as the body of the method. Notice that in our theoretical development we use unary methods, without loss of generality: tuples of arguments can be modelled by an object that instantiates a “special” class containing as fields all the needed arguments. Expressions e include variables, constants, field access, method call and object creation.

Following FJ [17], we rule out ill-formed programs, such as declaring a constructor named B within a class named A, or multiple fields or methods having the same name, or fields having the same type as the class they are defined in.

3 The SFJ Language

3.1 On Valid Type Definitions

Since we want to use types \(\tau \) to program in SFJ, we restrict them to finite trees whose leaves are basic types \({\mathbb B}\) Sect. 2.2 with no cycles. For example, a recursive type \(\alpha = [a : \alpha ]\) denotes an infinite program tree new C(new C(\(\cdots {}\))), hence we rule it out as it is not inhabitable. Similarly, the types \(\alpha = [b: \beta ]\), \(\beta = [a = \alpha ]\) create a cycle and thus would not be inhabitable. Notice that these types can be defined and inhabited in Java by assigning null to all fields in a class, however they are not useful in practice.

SFJ is implemented using ANTLR [24]. We start by defining the grammar of the language in Extended Backus-Naur Form (EBNF), following Sect. 2.1 and by running ANTLR, we can automatically generate a parser for SFJ and extend it in order to implement the required checks for our types and type system.

Running the parser on an SFJ program returns an abstract syntax tree (AST) of that program. When visiting the AST, we check if the program is well-formed, following the intuition at the end of Sect. 2. We mark any classes containing only fields typed with basic types as resolved, otherwise we mark them as unresolved. Using this information, Algorithm 1 checks if the type definitions in a program are valid, namely if they are finite trees whose leaves are basic types with no cycles. The algorithm returns True only if all the types in the SFJ program are resolved, otherwise it returns False, meaning there is at least one type definition which is invalid and contains a cycle.

figure b

3.2 Building Semantic Subtyping for SFJ

If Algorithm 1 returns True, meaning all type definitions in a program are valid, we can then build the semantic subtyping. Leveraging the interpretation of types as sets of values to define semantic subtyping for FJ [11, 12], in SFJ we keep track of the semantic subtyping relation by defining a map from a type to the set of its subtypes, satisfying the property that the set of values of a subtype is included in the set of values of the type.

We start with basic types and let Universe be a supertype of all types. The full mapping for basic types is defined in Map 3.1.

(3.1)

Note that Int is not a subtype of Float as a 32-bit float cannot represent the whole set of 32-bit integer values accurately and therefore Int is not fully set-contained in Float, however this is not the case for Int and Double. Similarly, Long is not a subtype of Double.

Algorithm 2 builds the semantic subtyping relation for all class types of an SFJ program by calling the function generateRelation. Given that classes are valid type definitions by Algorithm 1, we are guaranteed that Algorithm 2 will terminate.

The semantic subtyping generated by Algorithm 2 is a preorder: it is reflexive and transitive. This is also illustrated by Map 3.1.

figure c
figure d

Some comments on Algorithm 2 follow. In function generateRelation we iterate over the set of classes in an SFJ program. If the class currently being processed contains types in its fields or methods not present in the subtyping relation (lines 5 and 30, 42 in the continuation of the algorithm in the next page), then we add the current class to the list of unprocessed classes (line 6) so we can process its fields and methods first and the class itself later after having all required type information. The set of unprocessed classes will then be inspected again in a recursive call (line 10).

The next two functions of the algorithm, addClass and checkSuperSet given in the next page, check subtyping for the current class being processed and update relation, which is a mapping from a type to its subtypes and originally only consists of entries from Map 3.1. In function addClass(class) we check if the type class is a subtype of an existing type in relation (lines 15–18), as well as the opposite, meaning if class is a supertype of an existing type in relation (line 19). In order to do so checkSuperSet checks all fields (lines 28–39) and all methods (lines 40–51) in class and compares them with an existingClass in relation. If a subtyping relation is established, then it is added to relation (line 53). Finally, upon returning from checkSuperSet, we also add class to its own relation (line 21) to satisfy reflexivity and to Universe (line 22), which is a supertype of all types.

It is worth noticing that the subtyping algorithm finds all nominal and structural subtypes of a given type. This is due to the fact that all pairs of types are inspected. Recall from Sect. 1 that nominal subtyping is name-based and given by the class hierarchy defined by the programmer, whereas structural subtyping is structure-based and given by the set-inclusion of fields and methods. In particular, structural subtyping is contra-variant with respect to this set-inclusion. Algorithm 2 finds all structural subtypes of a given class because it checks that its fields and methods are a superset of existing types in relation. For example, all classes are structural subtypes of type \(empty = []\). On the other hand, it also finds all nominal subtypes because a class inherits all fields and methods of its superclass and as such its fields and methods are a superset of its superclass. This means that checking for structural subtyping is enough because nominal subtyping will be captured due to inheritance of fields and methods.

Finally, a note on complexity. The complexity of Algorithm 1 is \(\mathcal {O}(n)\), and the complexity of Algorithm 2 is \(\mathcal {O}(n^{2})\), with n being the size of the input. The reason for a quadratic complexity of Algorithm 2 is due to the symmetric check of structural subtyping between a class and an existingClass in relation. Notice that if we were to only work with nominal subtyping, then we would only require traversing the class hierarchy once, which gives an \(\mathcal {O}(n)\) complexity.

3.3 Type System for SFJ

The type system for the SFJ language, given in Sect. 2.2, is based on the type system by Dardha et al. [11, 12] where the formal typing rules and soundness properties are detailed. As these formal developments are beyond the scope of this paper, we discuss typing for SFJ only informally.

A program \((\tilde{L},e)\) is well typed if both \(\tilde{L}\) and e are well typed. Class declaration L and method declaration M are well typed if all their components are well typed. Let us move onto expressions E. Field access e.a, method call e.m(e) and object creation \(\mathbf {new}\ C(\widetilde{e})\) are typed in the same way as in Java: we inspect the type of the field and the type of the method and its arguments to determine the type of the field access and method call, respectively. The type of an object creation is determined by the type of its class. Regarding constants, in order to respect the set-theoretic interpretation of types as sets of values, we type constants with the most restrictive type, i.e., the type representing the smallest set of values containing the value itself. For example, the type system would assign to the value 42 the type byte, which is the smallest in the sequence byte, short, int (see Map 3.1 for details).

Finally, the subtyping relation generated by Algorithm 2 is used in the type system for the SFJ language via a subsumption typing rule:

$$ \frac{\varGamma \vdash e:\alpha _1 \qquad \alpha _1 \le \alpha _2}{\varGamma \vdash e:\alpha _2} $$

We read this typing rule as follows: if an expression e is of type \(\alpha _1\) under a typing context \(\varGamma \) (details of a typing context are irrelevant here) and type \(\alpha \) is a subtype \(\le \) of \(\alpha _2\), then expression e can be typed with \(\alpha _2\).

3.4 Polygons: Continued

Let us illustrate the semantic subtyping algorithm on our Polygons given in Example 1. Algorithm 2 generates the subtyping relation given in Map 3.2, together with the subtyping relation for basic types, omitted here and defined in Map 3.1. Notice that the mapping for Universe is extended with the new types for polygons.

(3.2)

Recall the method diagonal in class Diagonal, with signature

$$ \mathbf {double}\ diagonal((\textit{Polygon}\ \mathbf {and\ not}\ \textit{Triangle}) \ shape) $$

The result of the set operation on its parameter type gives the following set of polygons:

$$ Polygon\ \mathbf {and\ not}\ Triangle = \left\{ Polygon, Square, Rhombus \right\} $$

In order to define the not Triangle type we need the Universe type so that we can define it as \(Universe\ \mathbf {\setminus }\ Triangle\). Then, the and connective is the intersection of sets of Polygon with not Triangle.

If we write in our SFJ program the following expression:

$$ (\mathbf{new }\ Diagonal()).diagonal(\mathbf{new }\ Square()) $$

the argument new Square() of the diagonal method is of type Square, by the type system in Sect. 3.3 and Square is contained in the set of the parameter type of the method, so this expression will successfully type-checks.

However, if we write the following SFJ expression:

$$ (\mathbf{new }\ Diagonal()).diagonal(\mathbf{new }\ Triangle()) $$

Type Triangle is not contained in \(\left\{ Polygon, Square, Rhombus \right\} \), therefore this expression will not type-check and will return a type error at compile time.

This is further illustrated in the accompanying video of this paper [27].

3.5 Nominal vs. Structural Subtyping

In this section we will comment on pros and cons of nominal vs. structural subtyping.

Structural subtyping allows for more flexibility in defining this relation and the user does not need to explicitly definite it, as would do with nominal subtyping. However, for this flexibility we might need to pay in meaning. For example, consider the following two structurally equivalent classes, hence record types \(coordinate = [x:int, y:int, z:int]\) and \(colour = [x:int, y:int, z:int]\). While they can be used interchangeably in a type system using structural subtyping, their “meaning” is different and we might want to prohibit it, because intuitively speaking we do not want to use a colour where a coordinate is expected.

On the other hand, while nominal subtyping can avoid the above problem, it can introduce others and in particular, a developer can define an overridden method to perform the opposite logic to what the super class is expecting, as illustrated by the following classes in Java:

$$\begin{aligned} \begin{array}{ll} \mathbf {class} \ A \ \mathbf {extends }\ Object \ \{ &{} \qquad \mathbf {class} \ B \ \mathbf {extends }\ A\ \{ \\ \qquad \qquad \ldots \qquad &{} \qquad \qquad \qquad \ldots \\ \quad \mathbf{int }\ n;\qquad &{} \qquad \quad \mathbf{int }\ length()\{\ \mathbf {return}\ {-n};\ \} \\ \quad \mathbf{int }\ length()\{\ \mathbf {return}\ {n};\ \}\qquad &{} \qquad \} \\ \} \end{array} \end{aligned}$$

Both approaches have their pros and cons, and they leave an expectation on the developer to use the logic behind subtyping correctly when writing code. The integration of both subtyping approaches in SFJ gives the developer the freedom to choose the most suitable subtyping relation to use for a given task.

3.6 Methods in SFJ

On Multimethods. Since FJ is a core language, some features of the full Java are removed, such as overloading methods. In our framework, by leveraging the expressivity of boolean connectives and semantic subtyping, we are able to restore overloading, among other features [12, §8.4]. We can thus model multimethods, [5], which according to the authors is “very clean and easy to understand [...] it would be the best solution for a brand new language”. As an example, taken from Dardha et al. [11, 12], consider the following class declarations:

$$ \begin{array}{ll} \mathbf {class} \ A \ \mathbf {extends }\ Object \ \{ &{} \qquad \mathbf {class} \ B \ \mathbf {extends }\ A\ \{ \\ \qquad \quad \mathbf {int}\ length \ (\mathbf {string}\ s)\{\ \ldots \ \}\qquad &{} \qquad \qquad \quad \mathbf {int}\ length \ (\mathbf {int}\ n)\{\ \ldots \ \} \\ \} &{} \qquad \} \end{array} $$

Method length has type \(\mathbf {string} \rightarrow \mathbf {int}\) in class A. However, because class B extends class A, length has type \((\mathbf {string} \rightarrow \mathbf {int})\ \mathbf {and}\ (\mathbf {int} \rightarrow \mathbf {int})\) in class B, which can be simplified to \((\mathbf {string}\ \mathbf {or}\ \mathbf {int}) \rightarrow \mathbf {int}\).

Method Types. Let us illustrate the method types given in Sect. 2.1 via an alternative implementation of the class Diagonal at the end of Example 1.

figure e

We define the type of the (outside) diagonal method as accepting any type and its subtypes implementing the (inside) diagonal method with type signature void to double.

In order to type check an argument passed to the (outside) diagonal method, at compile time we build a collection of types \(\{type_{1},\ type_{2},\ldots \}\) which are class types where the (inside) diagonal method is defined. As such, we iterate over the list of classes in an SFJ program (as we did in Algorithm 2) to check for the required method. The resulting collection of types is the union of all classes where diagonal is defined together with their subtypes \(([\![type_{1}]\!] \cup [\![type_{2}]\!] \cup \ldots )\), where each \([\![type_{i}]\!]\) denotes a mapping of \(type_i\) to the set of its subtypes, similar to Map 3.2.

However, calculating this collection of types for each method of every class would be computationally inefficient and most importantly unnecessary as only few methods would in turn be used as method types. Therefore we only compute them on demand during type-checking when we come across such a type.

We can therefore use method types to statically include or exclude a portion of our class hierarchy. However, unlike with interfaces as in Example 1, the values that can be accepted by a method type do not have to be related to each other in any way in the class hierarchy. This indeed is useful if we are dealing with legacy code as we can still accept all classes where diagonal is defined, without having to go back and add interface implementations.

3.7 Code Generation

SFJ only includes the typechecking component of the language. In this section, we provide a sketch of the code generation algorithm, which is work in progress.

Given the similarity of SFJ to Java, our approach is to translate an SFJ program into Java bytecode and then run it on the Java Virtual Machine (JVM) [19]. This is a standard approach also used by other object-oriented languages, for example, KotlinFootnote 1.

The main challenge in translating SFJ into bytecode is translating types using boolean connectives. For example, a field \(f_1\) of type int or bool, will be translated as two Java fields, one of type int and one of type bool, and only one of the two types will be inhabited by a value. In order to achieve this, we first analyse our program and reduce the boolean types by keeping only the alternatives which actually get used in the program. For example, if the field of type int or bool only ever gets initialised with a boolean value, we can reduce it and make it a field of a single type bool. After this reduction phase, we then consider the remaining types which use boolean connectives and could not be reduced. On the example above, consider again field \(f_1\) of type int or bool. This will be translated as two fields \(\mathbf{int }\_{f_1}\) and \(\mathbf{bool }\_{f_1}\) with the corresponding types. In order to initialise these fields, we use the constructor overloading capabilities of the JVM to generate an overloaded version for each alternative type. In each constructor, only the field that matches the type of the parameter is initialised with all other fields set to null. To access the field of an object, we generate code that checks each alternative of the field if it is non-null and includes the rest of the code generation for the expression for each branch. At run time, only one branch will be true, and this is the branch of generated code which will be executed.

For methods, we also use the overloading capabilities of the JVM to define an overloaded method for each type in the expanded method parameter, all with the same method body. Depending on which alternative the argument inhabits at run time, a different method will be dispatched to. Like methods with boolean types, we similarly implement methods with method types, as we discussed in Sect. 3.6, by defining an overloaded alternative for each type that implements the specified method. This concludes the code generation phase for all expressions in SFJ given in Sect. 2.2.

4 Related Work and Conclusion

Semantic subtyping goes back to more than two decades ago [1, 10]. Hosoya and Pierce [14,15,16] define XDuce, an XML-oriented language designed specifically to transform XML documents in other XML documents satisfying certain properties. Frisch et al. [13] extend XDuce by introducing less XML specific types such as records, boolean connectives and arrow types, and implement it as \(\mathbb {C}\)Duce. Their work is similar to ours in that our class-based semantic type system is a combination of the \(\mathbb {C}\)Duce record types with arrow types. Castagna et al. define \(\mathbb {C}\pi \) [7], a variant of the asynchronous \(\pi \)-calculus, where channel types are augmented with boolean connectives; semantic subtyping for ML-like languages [8] and semantic subtyping in a gradual typing framework [6]. Ancona and Lagorio [3] define subtyping for infinite types by using union and object type constructors, where types are interpreted as sets of values of the language. Bonsangue et al. [4] study a coalgebraic approach to coinductive types and define a set-theoretic interpretation of coinductive types with union types. Pearce [26] defines semantic subtyping for rewriting rules in the Whiley Rewrite Language and for a flow-typing calculus [25].

Regarding implementations of semantic subtyping, to the best of our knowledge, there are only a few works in the literature. Muehlboeck and Tate [23] define a syntactic framework with boolean connectives which has been implemented in the Ceylon programming language [18]. Ancona and Corradi [2] define semantic subtyping for an imperative object-oriented language with mutable fields. In our framework we are considering only the functional fragment of Java, which is FJ, and as a result the semantic subtyping framework is simpler. The authors also propose a prototype implementation of their subtyping algorithm. Chaudhuri et al. [9] present the design and implementation of Flow, which is a type checker for JavaScript. They use boolean connectives and, not, or for their predicates, however they do not define semantic subtyping for their language.

In this paper we presented the design and implementation of SFJ—Semantic Featherweight Java, an extension of Featherweight Java featuring boolean types, semantic subtyping, and integrating both nominal and structural subtyping. Due to the expressivity of semantic subtyping, in SFJ we are able to restore standard Java constructs and features for example, lists and overloading meathods, which were not present in FJ, thus making SFJ a more complete language. We presented Algorithm 1 on validity of type definitions and Algorithm 2 on semantic subtyping, which finds all nominal and structural subtypes for all types in an SFJ program. We also described typing of terms in SFJ, which follows that of Java and builds upon relevant work [11, 12]. As future work, we aim to finalise the code generation phase, which is sketched in Sect. 3.7.