Artem Usov

Ornela Dardha
email: ornela.dardha@glasgow.ac.uk

SFJ: An implementation of Semantic Featherweight Java

Keywords: Nominal subtyping, Structural subtyping, Semantic Featherweight Java, Object-oriented languages, Boolean types, Type theory

 defined boolean types and semantic subtyping for Featherweight Java (FJ) and integrated both nominal and structural subtyping, thus exploiting the benefits of both approaches. However, these benefits were illustrated only at a theoretical level, but not exploited practically. We present SFJ-Semantic Featherweight Java, an implementation of FJ which features boolean types, semantic subtyping and integrates nominal as well as structural subtyping. The benefits of SFJ, illustrated in the paper and the accompanying video (with audio/subtitles) [27], show how static type-checking of boolean types and semantic subtyping gives higher guarantees of program correctness, more flexibility and compactness of program writing.

Introduction

There are two approaches to defining subtyping relations: the syntactic and the semantic approach. Syntactic subtyping [START_REF] Liskov | A behavioral notion of subtyping[END_REF] is more mainstream in programming languages and is defined by means of a set of formal deductive subtyping rules. Semantic subtyping [START_REF] Aiken | Type inclusion constraints and type inference[END_REF][START_REF] Damm | Subtyping with union types, intersection types and recursive types[END_REF] 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 [START_REF] Malayeri | Integrating nominal and structural subtyping[END_REF][START_REF] Malayeri | Is structural subtyping useful? an empirical study[END_REF]. 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. [START_REF] Dardha | Semantic Subtyping for Objects and Classes[END_REF][START_REF] Dardha | Semantic Subtyping for Objects and Classes[END_REF] define boolean types-based on set-theoretic operations such as and, not, or-and semantic subtyping for Featherweight Java (FJ) [START_REF] Igarashi | Featherweight java: a minimal core calculus for java and gj[END_REF]. 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 § 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, §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 [START_REF] Boyland | Parasitic methods: An implementation of multimethods for java[END_REF], 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 [START_REF] Usov | SFJ: An implementation of Semantic Featherweight Java[END_REF] to illustrate the benefits of boolean types and semantic subtyping developed by Dardha et al. [START_REF] Dardha | Semantic Subtyping for Objects and Classes[END_REF][START_REF] Dardha | Semantic Subtyping for Objects and Classes[END_REF] 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: 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 [START_REF] Usov | SFJ: An implementation of Semantic Featherweight Java[END_REF]: 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 § 2 we present the types and terms of the SFJ language. In § 3 we present the design and implementation of SFJ; we discuss our two main algorithms, Algo. 1 in § 3.1 which checks the validity of type definitions, and Algo. 2 in § 3.2 which generates the semantic subtyping relation. Further, we discuss typing of SFJ in § 3.3; nominal vs. structural subtyping in § 3.5; method types in § 3.6; and code generation in § 3.7. We discuss related work and conclude the paper in § 4.

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. [START_REF] Dardha | Semantic Subtyping for Objects and Classes[END_REF][START_REF] Dardha | Semantic Subtyping for Objects and Classes[END_REF], and SFJ builds on that framework.

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

Types

The syntax of types τ is defined by the following grammar:

τ ::= α | µ Types α ::= 0 | B | [ l : τ ] | α and α | not α Field types (α-types) µ ::= α → α | µ and µ | not µ Method types (µ-types)
The α-types are used to type fields and the µ-types are used to type methods. Type 0 is the empty type. Type B denotes the basic types, such as integers, booleans, etc. Record types [ l : τ ], where l is a sequence of disjoint labels, are used to type objects. Arrow types α → α are used to type methods.

The boolean connectives and and not in the α-types and µ-types have their expected set-theoretic meanings. We let α \ \ \ α denote α and (not α ), and α or α denote not(not α and (not α )).

Terms

The syntax of terms is defined by the following grammar and is based on the standard syntax of terms in FJ [START_REF] Igarashi | Featherweight java: a minimal core calculus for java and gj[END_REF]: We assume an infinite set of names, with some special names: Object denotes the root class, this denotes the current object and super denotes the parent object. We let A, B, . . . range over classes; a, b, . . . over fields; m, n, . . . over methods and x, y, z, . . . over variables.

A program ( L, e) is a pair of a sequence of class declarations 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 [START_REF] Igarashi | Featherweight java: a minimal core calculus for java and gj[END_REF], 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

On Valid Type Definitions

Since we want to use types τ to program in SFJ, we restrict them to finite trees whose leaves are basic types B § 2.2 with no cycles. For example, a recursive type α = [a : α] denotes an infinite program tree new C(new C(• • • )), hence we rule it out as it is not inhabitable. Similarly, the types α = [b : β], β = [a = α] 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 [START_REF] Parr | The definitive ANTLR 4 reference[END_REF]. We start by defining the grammar of the language in Extended Backus-Naur Form (EBNF), following § 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 § 2. We mark any classes containing only fields typed with basic types as resolved, otherwise we mark them as unresolved. Using this information, Algo. 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 T rue only if all the types in the SFJ program are resolved, otherwise it returns F alse, meaning there is at least one type definition which is invalid and contains a cycle.

Building Semantic Subtyping for SFJ

If Algo. 1 returns T rue, 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 [START_REF] Dardha | Semantic Subtyping for Objects and Classes[END_REF][START_REF] Dardha | Semantic Subtyping for Objects and Classes[END_REF], 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 U niverse be a supertype of all types. The full mapping for basic types is defined in Map 3.1.

Double = {Double, F loat, Int, Short, Byte} F loat = {F loat, Short, Byte} Long = {Long, Int, Short, Byte} Int = {Int, Short, Byte} Short = {Short, Byte} Byte = {Byte} Boolean = {Boolean} V oid = {V oid} U niverse = {Double, F loat, Long, Int,
Short, Byte, Boolean, V oid} (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 setcontained in Float, however this is not the case for Int and Double. Similarly, Long is not a subtype of Double.

Algo. 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 Algo. 1, we are guaranteed that Algo. 2 will terminate. The semantic subtyping generated by Algo. 2 is a preorder: it is reflexive and transitive. This is also illustrated by Map 3.1.

Some comments on Algo. 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 [START_REF] Hosoya | Xduce: A statically typed xml processing language[END_REF][START_REF] Hosoya | Regular expression types for xml[END_REF][START_REF] Igarashi | Featherweight java: a minimal core calculus for java and gj[END_REF][START_REF] King | The Ceylon Language Specification, Version 1[END_REF], as well as the opposite, meaning if class is a supertype of an existing type in relation (line [START_REF] Lindholm | The Java Virtual Machine Specification[END_REF]. 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 U niverse (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 § 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 par-Algorithm 2: Semantic Subtyping for SFJ-addClass and checkSuperSet /* ...algorithm continued from previous page */ ticular, structural subtyping is contra-variant with respect to this set-inclusion. Algo. 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 Algo. 1 is O(n), and the complexity of Algo. 2 is O(n 2 ), with n being the size of the input. The reason for a quadratic complexity of Algo. 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 O(n) complexity.

Type System for SFJ

The type system for the SFJ language, given in § 2.2, is based on the type system by Dardha et al. [START_REF] Dardha | Semantic Subtyping for Objects and Classes[END_REF][START_REF] Dardha | Semantic Subtyping for Objects and Classes[END_REF] 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 ( L, e) is well typed if both 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 new C( 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 Algo. 2 is used in the type system for the SFJ language via a subsumption typing rule:

Γ e : α 1 α 1 ≤ α 2 Γ e : α 2
We read this typing rule as follows: if an expression e is of type α 1 under a typing context Γ (details of a typing context are irrelevant here) and type α is a subtype ≤ of α 2 , then expression e can be typed with α 2 . The result of the set operation on its parameter type gives the following set of polygons: P olygon and not T riangle = {P olygon, Square, Rhombus}

Polygons: Continued

In order to define the not T riangle type we need the U niverse type so that we can define it as U niverse \ T riangle. Then, the and connective is the intersection of sets of P olygon with not T riangle.

If we write in our SFJ program the following expression:

(new Diagonal()).diagonal(new Square())
the argument new Square() of the diagonal method is of type Square, by the type system in § 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:

(new Diagonal()).diagonal(new T riangle())
Type T riangle is not contained in {P olygon, Square, Rhombus}, 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 [START_REF] Usov | SFJ: An implementation of Semantic Featherweight Java[END_REF].

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:

class A extends Object { class B extends A { . . . . . . int n; int length(){ return -n; } int length(){ return n; } } }
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.

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, [START_REF] Boyland | Parasitic methods: An implementation of multimethods for java[END_REF], 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. [START_REF] Dardha | Semantic Subtyping for Objects and Classes[END_REF][START_REF] Dardha | Semantic Subtyping for Objects and Classes[END_REF], consider the following class declarations: 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 , . . .} 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 Algo. 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 ]] ∪ [[type 2 ]] ∪ . . .), 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 Ex. 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.

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) [START_REF] Lindholm | The Java Virtual Machine Specification[END_REF]. This is a standard approach also used by other object-oriented languages, for example, Kotlin 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 int_f 1 and 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.

1 https://kotlinlang.org/ 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 § 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 § 2.2.

Related Work and Conclusion

Semantic subtyping goes back to more than two decades ago [START_REF] Aiken | Type inclusion constraints and type inference[END_REF][START_REF] Damm | Subtyping with union types, intersection types and recursive types[END_REF]. Hosoya and Pierce [START_REF] Hosoya | Regular expression pattern matching for xml[END_REF][START_REF] Hosoya | Regular expression types for xml[END_REF][START_REF] Hosoya | Xduce: A statically typed xml processing language[END_REF] define XDuce, an XML-oriented language designed specifically to transform XML documents in other XML documents satisfying certain properties. Frisch et al. [START_REF] Frisch | Semantic subtyping: Dealing settheoretically with function, union, intersection, and negation types[END_REF] extend XDuce by introducing less XML specific types such as records, boolean connectives and arrow types, and implement it as CDuce. Their work is similar to ours in that our class-based semantic type system is a combination of the CDuce record types with arrow types. Castagna et al. define Cπ [START_REF] Castagna | Semantic subtyping for the pi-calculus[END_REF], a variant of the asynchronous π-calculus, where channel types are augmented with boolean connectives; semantic subtyping for ML-like languages [START_REF] Castagna | Set-theoretic types for polymorphic variants[END_REF] and semantic subtyping in a gradual typing framework [START_REF] Castagna | Gradual typing with union and intersection types[END_REF]. Ancona and Lagorio [START_REF] Ancona | Coinductive subtyping for abstract compilation of objectoriented languages into horn formulas[END_REF] 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. [START_REF] Bonsangue | A coalgebraic foundation for coinductive union types[END_REF] study a coalgebraic approach to coinductive types and define a set-theoretic interpretation of coinductive types with union types. Pearce [START_REF] Pearce | On declarative rewriting for sound and complete union, intersection and negation types[END_REF] defines semantic subtyping for rewriting rules in the Whiley Rewrite Language and for a flow-typing calculus [START_REF] Pearce | Sound and complete flow typing with unions, intersections and negations[END_REF].

Regarding implementations of semantic subtyping, to the best of our knowledge, there are only a few works in the literature. Muehlboeck and Tate [START_REF] Muehlboeck | Empowering union and intersection types with integrated subtyping[END_REF] define a syntactic framework with boolean connectives which has been implemented in the Ceylon programming language [START_REF] King | The Ceylon Language Specification, Version 1[END_REF]. Ancona and Corradi [START_REF] Ancona | Semantic subtyping for imperative object-oriented languages[END_REF] 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. [START_REF] Chaudhuri | Fast and precise type checking for javascript[END_REF] 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 Algo. 1 on validity of type definitions and Algo. 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 [START_REF] Dardha | Semantic Subtyping for Objects and Classes[END_REF][START_REF] Dardha | Semantic Subtyping for Objects and Classes[END_REF]. As future work, we aim to finalise the code generation phase, which is sketched in § 3.7.

  Class declaration L ::= class C extends C { α a; K; M } Constructor K ::= C ( α x) { super( x); this.a = x; } Method declaration M ::= α m (α x) { return e; } Expressions e ::= x | c | e.a | e.m(e) | new C( e)

Algorithm 1 :

 1 Validity Check for Type DefinitionsInput : classes, the set of classes in an SFJ program marked resolved, if their fields contain only basic types, unresolved otherwise. Output : T rue if all classes are valid type definitions, F alse otherwise.

4 for

 4 class that is unresolved in classes do 5 resolved ←-T rue 6 for field in class that contains a class type do 7 if type of field is unresolved then 8 resolved ←-F alse 9 end 10 end 11 12 if resolved = T rue then 13 class ←-resolved 14 resolutionOccured ←-T rue 15 end

Algorithm 2 : 2 Function 4 for class in classes do 5 if 6 unprocessed 13 /

 2245613 Semantic Subtyping for SFJ-generateRelation Input : classes, the set of classes in an SFJ program. relation, the mapping of types to the set of subtypes, initially Map 3.1. 1 begin generateRelation(classes: List<Class>): 3 unprocessed : List < Class > ←-[] addClass(class) = F alse then * algorithm continued on next page... */

13 14FunctionFunction

 13 addClass(class: Class) → boolean: 15 for existing class type in relation do 16 if checkSuperSet(class, existingClass) = False then 17 checkSuperSet(class: Class, other: Class) → boolean: 27 f lag ←-T rue 28 for field in class do 29 if field contains type not in relation then 30 return F alse 31 end 32 if other does not contain field then 33 f lag ←-F alse 34 else 35 if other.field.types does not fully contain field.types then 36 f lag ←class do 41 if method contains type not in relation then 42 return F alse 43 end 44 if other does not contain method then 45 f lag ←-F alse 46 else 47 if other.method.types does not fully contain method.types then 48 f lag ←-

  Let us illustrate the semantic subtyping algorithm on our Polygons given in Ex. 1. Algo. 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 U niverse is extended with the new types for polygons. P olygon = {P olygon, T riangle, Square, Rhombus} T riangle = {T riangle} Square = {Square} Rhombus = {Rhombus} U niverse = {Double, F loat, Long, Int, Short, Byte Diagonal = {Diagonal} Boolean, V oid, P olygon, Square Square, Rhombus, Diagonal} (3.2) Recall the method diagonal in class Diagonal, with signature double diagonal((Polygon and not Triangle) shape)

  class A extends Object { class B extends A { int length (string s){ . . . } int length (int n){ . . . } } } Method length has type string → int in class A. However, because class B extends class A, length has type (string → int) and (int → int) in class B, which can be simplified to (string or int) → int. Method types Let us illustrate the method types given in § 2.1 via an alternative implementation of the class Diagonal at the end of Ex. 1. class Diagonal { . . . double diagonal((diagonal : void → double) shape) { return shape.diagonal(); } }

  class P olygon {. . .} class T riangle extends P olygon {. . .} class Other_P olygons extends P olygon { double diagonal(Other_P olygons shape) {. . .} . . . } class Square extends Other_P olygons {. . .} class Rhombus extends Other_P olygons {. . .} Or by means of an interface Diagonal : public interface Diagonal { double diagonal(P olygon shape); } class P olygon {. . .} class T riangle extends P olygon {. . .} class Square extends P olygon implements Diagonal {. . .} class Rhombus extends P olygon implements Diagonal {. . .} // other polygons . . . Now, suppose our class hierarchy is such that Polygon is the parent class

Supported by the UK EPSRC grant EP/K034413/1, "From Data Types to Session Types: A Basis for Concurrency and Distribution" (ABCD), and by the EU HORIZON 2020 MSCA RISE project 778233 "Behavioural Application Program Interfaces" (BehAPI).