Global type inference for Java is able to compute correct types for an input program which has no type annotations at all, but turns out to be NP-hard. Former implementations of the algorithm therefore struggled with bad runtime performance. In this original paper, we translate the type inference algorithm for Featherweight Generic Java to an Answer Set Program. Answer Set Programming (ASP) promises to solve complex computational search problems as long as they are finite domain. This paper shows that it is possible to implement global type inference for Featherweight Generic Java (FGJ) as an ASP program. Afterwards we compared the ASP implementation with our own implementation in Java showing promising results. Another advantage is that the algorithm's specification can be mapped directly to ASP code, which reduces the likelihood of errors in the implementation.
//
A possible input for our algorithm is shown in Figure 1. Here the method untypedMethod is missing its argument type for var and its return type. Global type inference works in two steps. First we generate a set of subtype constraints, which are later unified resulting in a type solution consisting of type unifiers . Every missing type is replaced by a type placeholder. In this example the type placeholder var is a placeholder for the type of the var variable. The ret placeholder represents the return type of the untypedMethod method. Also shown as a comment behind the respective method call. There are two types of type constraints: • A subtype constraint such as var ⋖ C1 indicates that the unification algorithm must determine a type substitution for var that is a subtype of C1. One possible solution would be (var ) = C1.
.
• A equals constraint var = C1, which results in (ret ) = C1.
Our type inference algorithms for Java are described in a formal manner in [
The nature of the global type inference algorithm causes the search space of the unification algorithm to increase exponentially with every ambiguous method call. Java allows overloaded methods, causing our type inference algorithm to create so-called Or-Constraints. This happens if multiple classes implement a method with the same name and the same amount of parameters. Given the input program in Figure 1, we do not know, which method self is meant for the method call var.self(), because there is no type annotation for var.
. .
An Or-Constraint like {var ⋖ C1, ret = C1.} || {var ⋖ C2, ret = C2} means that either the constraint set {var ⋖ C1, ret =. C1} or {var ⋖ C2, ret = C2} has to be satisfied. If we set the type of var to C1, then the return type of the method will be C1 as well. If we set it to C2, then the return type will also be C2. Since two distinct possibilities exist, an Or-Constraint with both variants is required. untypedMethod(var){
return var.self().self().self().self(); }
If we chain multiple overloaded method calls together, we end up with multiple Or-Constraints.
The type unification algorithm Unify only sees the supplied constraints and has to potentially try all
combinations of them. This is proven in [
Let’s have a look at the following alternation of our example shown in Figure 2. Now there are four chained method calls leading to four Or-Constraints: {var ⋖ C1, r1 =. C1} || {var ⋖ C2, r1 =. C2} {r1 ⋖ C1, r2 =. C1} || {r1 ⋖ C2, r2 =. C2} {r2 ⋖ C1, r3 =. C1} || {r2 ⋖ C2, r3 =. C2}
. .
{r3 ⋖ C1, ret = C1} || {r3 ⋖ C2, ret = C2}
The placeholder r1 stands for the return type of the first call to self and r2 for the return type of
the second call and so on. It is obvious that this constraint set only has two solutions. The variable var
and the return type of the method as well as all intermediate placeholders r1 − r3 get either the type
C1 or C2. A first prototype implementation of the Unify algorithm [
Our global type inference algorithm should construct type solutions in real time. Then, it can efectively be used as a Java compiler which can deal with large inputs of untyped Java code. Another use case scenario is as an editor plugin which helps a Java programmer by enabling him to write untyped Java code and letting our tool insert the missing type statements. For both applications, a short execution time is vital.
Answer Set programming promises to solve complex search problems in a highly optimized way.
The idea in this paper is to implement the algorithm presented in [
The original global type inference algorithm used by the Java-TX1 project proceeds in two phases: (1) generate a set of subtype constraints, and (2) unify them to obtain a substitution mapping type placeholders to types.
This type unification for Java has been studied in several works. Plümicke [
Type unification is the process of finding substitutions for type variables so that two given type terms become compatible under a specified compatibility relation. Formally, given two type terms 1 and 2, the type unification problem is to find a substitution mapping type placeholders to type terms such that:
( 1) ≤ * ( 2). where ≤ * is the transitive closure of the Java subtype relation.
Our ASP implementation realizes the algorithm of [
Answer Set Programming has a declarative way of formulating search problems. In ASP you encode
the problem as a set of logical rules and facts and let an ASP solver (like clingo2) compute one or
more stable models (also called answer sets). A stable model is a self-justifying, minimal3, and internally
consistent interpretation of the program [
Translated to our algorithm, this means that the input set of constraints are the facts and the implication rules shown in Figure 5 are the logic rules. Thus, a stable model must be a constraint set that satisfies all the rules, contains the input set of constraints, and is minimal (see definition 1). Furthermore, the rules of our algorithm Ω are formulated in a way that each input set of constraints either ends in a fail condition — meaning there is no possible solution — or leads to a stable model that contains correct unifiers of the form (a) = G for every type placeholder a in the input constraints.
1https://www.dhbw-stuttgart.de/horb/forschung-transfer/forschungsschwerpunkte/typsysteme-fuer-objektorientierte-pro grammiersprachen/
::= T, S ::= N ::= G ::= P ::= .
T ⋖ T | T = T a | N C<P> C<G> a | G
G are types that contain no type placeholders. A type P is either a type placeholder or a type not containing type placeholders at all. The reason for those definitions is that they restrict type placeholder to only appear in the uppermost level of a type parameter list.
Definition 1 (Stable Model). A stable model (or answer set) of an input set is a set of constraints with ⊆ that: • Satisfies all the rules • Is complete: If the premise of any rule in Ω is satisfied by elements of , then the conclusion of that rule must also be included in .
• Is minimal (no unnecessary atoms)
All extends relations in the input program have to satisfy the WF-Class rule. This restriction is necessary because our algorithm only supports type placeholders in the uppermost layer of a type parameter list. WF-Class rule ensures that supertypes generated by the Super rule are well-formed. For example the class definition class Matrix<A> extends List<List<A>> is not supported by our algorithm Ω. If an input contains a constraint Matrix<a> ⋖ b, then the Super rule would require for . a b = List<List<a>> constraint where the type List<List<a>> is not well-formed according to the rules in Figure 4 and therefore not supported by our algorithm.
S1, S2, T1, T2 ok . = {S1 = S2, T1 ⋖ T2} ok
C<P> ok WF-Var a ok
for any a :
([X/a]N) ok class C<X> ▷ N ok 4.1. Unification Algorithm All the implication rules depicted in this chapter can be translated to ASP statements as described in chapter 6. The whole algorithm is depicted in Figure 5
We need the Solution-Requirement rule to force at least one type solution for every type placeholder in the input constraints (see example 4.1).
Example 4.1: Solution-Requirement a ⋖ List<x >, a ⋖ List<String>. We want our program to create a unifier for a which requires at least one constraint of the form a =. . . .. Solution-Requirement forces the ASP solver to choose one of the following possibilities: a ⋖ List<x >, a ⋖ List<String> a =. List<x > a =. List<String> In this case, it does not matter which one gets chosen as they will both lead to the same result. Let’s take the a =. List<x > for example. Then we end up with a constraint List<x > ⋖ List<String> Unify:
T <: T
T1 <: T2 T2 <: T3 T1 <: T3
class C<X> ▷ N C<T> <: [T/X]N Sau=b.stT-1L
a ⋖ T2 T1 ⋖ T2 Sau=b.stT-1R
T2 ⋖ a T2 ⋖ T1 Sau=b.stG-Param .
T = C<P1 . . . , a, . . . Pn> .
T = C<P1, . . . G, . . . Pn> Sau=b.stG-Param-Left
C<P1 . . . , a, . . . Pn> ⋖ b C<P1, . . . G, . . . Pn> ⋖ b Reduce .
C<P1 . . . Pn> = C<P′1 . . . P′n> P =. P′
a ⋖ Object
N ⋖ a Solution: Fail Conditions: Soalu=.tioGn (a) = G
C< . . . > ⋖ D< . . . > Anti Circle Conditions: Bau=i.ldC< . . . , b, . . . > a → b
a → b b → c a → c
Sau=b.stT-1Equala =. T2 .
T1 = T2
.
T1 = T2
.
T2 = T1 Sau=b.stG-Param-Right b ⋖ C<T1 . . . , a, . . . Tn> b ⋖ C<P1, . . . G, . . . Pn>
N ⋖ C<P1 . . . Pn> N <: C<P′1 . . . P′n> . .
P1 = P′1 . . . P = P′
N <: N1, . . . , N <: N for one ∈ {1, . . . , } :
N1, . . . , N ok a =. N
a ⋖ N1, . . . , a ⋖ N there must exist at least one :
.
C< . . . > = D< . . . > a =. N C ̸= D ∅
a → a fail due to Subst-L. Adapt creates a List<x > =. List<String> constraint and from there we get . . . x = String by Reduce. Together with a = List<x > this leads to a = List<String> (by
4.2. Diferences to the Featherweight Generic Java Type Unification
The ASP unify algorithm Ω presented here is a toned down version of the algorithm presented in
[
The Scala prototype of the Unify algorithm, provided with [
Our ASP implementation on the other hand does not use any state and therefore cannot change an existing constraint set. All possible substitutions are laid out by the grounding process. Afterwards all incorrect solutions are ruled out. This allows for a more declarative programming style, where we specify the type rules and let ASP Figure out a solution for itself.
Given a set of constraints and our algorithm Ω as input, the ASP solver attempts to find the smallest possible set of constraints . This set contains the input constraints and satisfies all implication rules shown in Figure 5. The constraint set is also called a stable model (see Definition 1). We proved two key properties of : soundness and completeness.
Soundness All produced typings respect the original constraints; the algorithm never returns an incorrect assignment.
Completeness If a solution exists, the procedure finds one, as long as the input set does not contain circles (Def. 2) See the Full Paper for a detailed version of the proofs.
Definition 2 (Circular Constraint). A set of constraints a =. N where ∀N ∈ N : fv(N) ̸= ∅ and a contains all type placeholders used in N (meaning a = fv(N)) is called a circle.
Note: See the Full Paper for the complete program including an example input ASP statements consist of a head and a body separated by a implication operator ":-": head :- body. This statement is interpreted as an implication rule. If the premises in the body are satisfied, the facts stated in the head are deducted. The implication rules defined in Figure 5 are formulated in a way that can be translated to an ASP program. This chapter explains how to code our algorithm Ω in ASP. At ifrst, we give a ASP representation for each syntax element used in Figure 3:
C<Object> =⇒ type("C", params(Object, null))
a ⋖ b =⇒ subcons(tph("a"), tph("b"))
List<a> =⇒ type("List", params(tph("a")))
In addition to the constraint set , our algorithm requires the class inheritance information of all classes that appear in the constraints. This information is essential for evaluating subtype relationships and is encoded in the form of ASP rules. Specifically, for every class declaration in the Java type system of the form class C<X> extends D<X> we generate a corresponding ASP rule:
subtype(type("C", params(X)), type("D", params(X)))
:- subtype(type("C", params(X))).
These rules capture the inheritance hierarchy and serve as a static input to the algorithm, just like the constraint set . Thus, the complete input to our algorithm consists of: • The set of type constraints • The set of ASP rules encoding all relevant extends relations
This inheritance information is especially relevant for the Super and Adapt rules, both of which contain premises of the form N <: D< . . . >. For example, when the input set contains a constraint like a ⋖ N, the algorithm must determine the supertypes of N in order to apply the Super rule. This is exactly where the encoded inheritance rules come into play. The following example 6.1 illustrates this process in practice.
Example 6.1: Creating Supertypes
and let the constraint set be We need a helper rule in our ASP program that looks like this: subtype(type(A, P)) :- subcons(type(A, P), _).
class Vector<X> extends List<X>, = { Vector<String> ⋖ a }. subtype(type("Vector", params(type("String", null)))). subcons(type("Vector", params(type("String", null))), tph("a")).
subtype(type("Vector", params(type("String", null))), type("List", params(type("String", null)))).
Vector<String> <: List<String>.
With this information, the Super rule (see Listing 2) can select a valid supertype for a. In this case, it yields the ASP fact: equalcons(tph("a"),
type("List", params(type("String", null)))). which corresponds to the constraint a =. List<String>.
{equalcons(tph(A), type(D,DP)): subtype(type(C,CP), type(D,DP))}=1 :- subcons(type(C, CP), tph(A)).
subcons(A,B); orCons(C,D) :- orCons(subcons(A,B), subcons(C,D)). The operator ";" tells ASP to consider either the left or the right side. By supplying multiple OrConstraints this way, the ASP interpreter will consider all combinations, the Cartesian product of the
The rules implying a failure ∅ are translated by leaving the head of the ASP statement empty. If the body of such rules is satisfied, the algorithm considers the deduction as incorrect. See an example in
:- equalcons(type(A, _), type(B, _)), A != B.
To evaluate the performance and practical applicability of our ASP implementation of the Unify algorithm for FGJ, we conducted two benchmarks: 1. Massive Or-Constraints: Tests Unify’s ability to create and handle Cartesian products of big
2. Matrix Example: Typical benchmark used to test Java-TX type inference, where the Unify algorithm has to consider many possible variations of supertypes of the class Matrix.
Even though import statements in standard Java are purely syntactic and used only to avoid writing fully qualified class names, the current Java-TX implementation uses them to limit the search space for missing type annotations. The algorithm only considers “imported” types. This makes Java-TX type inference unsuitable for typical Java development, where users expect to reuse classes without needing to import them in advance. In contrast, our ASP-based Unify algorithm aims to lift this restriction by considering the entire standard Java library as potential type candidates. To demonstrate this, we introduce the following benchmark program shown in Listing 4:
Listing 4: Benchmark public class ThreeAdds { void addTest(a, b, c, d){ a.add(b); b.add(c); c.add(d); d.add(a); }
}
The addTest declaration in Listing 4 is missing type annotations for its parameters a,b,c,d. We want our ASP implementation of the Unify algorithm to calculate all possible typings for the missing type annotations. Therefore, we have to first generate a set of constraints representing the input problem. The method addTest has three calls a.add(...), which leads to three large Or-Constraints. We use the Open-JDK standard library of the version 21, which contains nearly twenty thousand classes, including inner classes. They have 200 diferent add methods all together. This leads to four Or-Constraints with 200 possibilities, meaning a Cartesian product with 1.6 billion elements. clingo ifnds a solution in under half a second.
Listing 5: Solution for Benchmark 4 public class ThreeAdds { void addTest(javax.naming.directory.Attribute a, java.util.concurrent.DelayQueue b, The program in Listing 4 admits an unexpectedly large number of valid type solutions, as many add methods in the Java standard library accept Object as an argument. One such solution is shown in Listing 5 and compiles under OpenJDK 17. We assume clingo spends most time in grounding, since ifnding a single valid typing is trivial once all possibilities are enumerated.
The second benchmark, the Matrix example shown in Listing 6, is also used by the Java-TX project
as a functionality demo and stress test. The grayed-out types in the method header are to be inferred
by our algorithm, including those omitted via Java’s var keyword [
class Matrix extends Vector<Vector<Integer>> { Matrix mul(Matrix m) { var ret = new Matrix(); var i = 0; while(i < size()) { var v1 = this.elementAt(i); var v2 = new Vector<Integer>(); var j = 0; while(j < v1.size()) { var erg = 0; var k = 0; while(k < v1.size()) { erg = erg + v1.elementAt(k)
* m.elementAt(k).elementAt(j); k++; } v2.addElement(new Integer(erg)); j++; } ret.addElement(v2); i++; } return ret; } }
ASP handles Or-Constraints eficiently. We evaluated our ASP-based unification algorithm on an extended version of the constraints from Figure 2, increasing the complexity by adding stacked method calls. Even with ten such calls, clingo succeeded in under 50 ms, whereas the current Java implementation4 required several seconds for the same input.
It is important to note that this benchmark avoids wildcard types to ensure a fair comparison, as the
Java implementation supports them, whereas the ASP version does not. In this first study on applying
ASP to Java type inference, wildcard types were deliberately omitted. Including wildcards makes subtype
checking in Java Turing complete [
In preparation of this work, the authors used AI-based tools for spell and grammar checking. All ideas and results presented are our own and we take full responsibility for the accuracy and integrity of the publication.