Understanding constraint formula concept in Java

Question

JLS defined a concept called "constraint formula". There is a formal definition:

Constraint formulas are assertions of compatibility or subtyping that may involve inference variables. The formulas may take one of the following forms:

• ‹Expression → T›: An expression is compatible in a loose invocation context with type T (§5.3).

• ‹S → T›: A type S is compatible in a loose invocation context with type T (§5.3).

• ‹S <: T›: A reference type S is a subtype of a reference type T (§4.10).

• ‹S <= T›: A type argument S is contained by a type argument T (§4.5.1).

• ‹S = T›: A reference type S is the same as a reference type T (§4.3.4), or a type argument S is the same as type argument T.

• ‹LambdaExpression →throws T›: The checked exceptions thrown by the body of the LambdaExpression are declared by the throws clause of the function type derived from T.

• ‹MethodReference →throws T›: The checked exceptions thrown by the referenced method are declared by the throws clause of the function type derived from T.

I have some misunderstanding about it. As far as I've understood we have a set of all Java types, denote it by M. Could we say, that any constraint formula defines a subset of M, for instance

‹S <: T› = {S | (S belongs to M) and (S is a subtype of T) }

Answer 1

First, not all of the constraint formulas work with types, some of them work with expressions, or other objects. For example, what would be the set for the formula ‹1+1 → Integer›?

Second, a formula might contain zero, one (at either position) or two inference variables (denoted by Greek letters). What would be the set for ‹String → Object›, ‹α → Object›, ‹String → α›, or ‹α → β›?

Third, I think you should think about constraint formulas as predicates, not as sets. For example, the formula ‹String <: Object› is satisfied, while ‹Object <: String› isn't.

And when you have a constraint formula with inference variables, you can start talking about sets of types (or sets of pairs of types for formulas with two variables) that satisfy the formula.

This means that I think that the closest you can get to your equation would be something like:

{α | ‹α <: T› } = {α | (α belongs to M) and (α is a subtype of T) }

(Though the second part is unnecessarily verbose, "α is a subtype of T" already implies "α belongs to M".)

Answer 2

Constraint formulas are assertions: they are either true or false (given a context where they are valid). For example, ‹byte → int› is true (in any valid context) because it is an instance of a widening primitive conversion which is a loose invocation context for the destination type. C1 is a subclass of C2, then ‹C1 <: C2› is true. On the other hand, ‹String <: int› is false, because there is no such subtype relation.

When a formula contains inference variables (which is the useful case), the truth value of the assertion depends on the value of the variable. The formula is a predicate: it can be seen as a function from the set of types to the set of booleans. This is equivalent to a set of types — the set of types for which the function is true. Thus a formula like ‹α <: String› can be seen as the set of subtypes of the String class type.

A formula containing multiple inference variables can likewise be interpreted as a set of tuples of types — a set of pair of types if there are two variables, a set of triples of types if there are three variables, etc.

In general, a formula can be interpreted as a set of lists of types, where each element of the list is the value of one variable. A formula contains a finite number of variables, therefore it is enough to consider finite lists. For example, the formula interface A {α₀ m(α₁ x, α₂ y);} → α₄ can be interpreted as the set of lists of types [T₀, T₁, T₂, T₃, T₄] such that interface A {T₀ m(T₁ x, T₂ y);} is compatible with a loose invocation context with type T₄.

Note that a formula is a syntactic object. The interpretation of a formula as a boolean or as a set is a denotational semantics for formulas. The JLS defines an operational semantics for constraint formulas, which consists of a reduction to bound sets.