=Paper=
{{Paper
|id=None
|storemode=property
|title=Inference, Targeting and Compatibility in a Type System for Java with SAM Typed Closures
|pdfUrl=https://ceur-ws.org/Vol-928/0049.pdf
|volume=Vol-928
|dblpUrl=https://dblp.org/rec/conf/csp/BelliaO12
}}
==Inference, Targeting and Compatibility in a Type System for Java with SAM Typed Closures==
https://ceur-ws.org/Vol-928/0049.pdf
Inference, Targeting and Compatibility in a Type
System for Java with SAM Typed Closures
Marco Bellia and M. Eugenia Occhiuto
Dipartimento di Informatica, Università di Pisa, Italy {bellia,occhiuto}@di.unipi.it
Abstract. In this paper we consider the new type structure that has been pro-
posed for Java closures, in the last Java Specification Language [BS11a]. This
structure uses SAM types that are in fact, nominal types instead of the struc-
tural, functional types, used in the previous, proposals. In addition, it allows
type inference for closures and for closure arguments. Through a technique, al-
ready consolidated in previous studies in Java extensions, we extend the calculus
FGJ, [IPW01], with interfaces, anonymous classes, closures of the new form and
SAM types. We define a type system and a reduction semantics for this calculus
FGATCJ. Using the type system, we formalize the notions of closure context,
target type, compatibility type and closure type as they emerge in [BS11a]. Even-
tually, we prove the soundness of the type system.
1 Introduction
The problem of extending Java with closures is widely discussed in several papers and
discussion forums (see [BO11,Ope12]). In this paper we prove type soundness for Java
closures in the last proposal of JSR 000335 [BS11a,BS11b]. Such a proposal uses SAM
types [BLB06] as types for closures, but shares with the previous proposals the idea
of considering closures as a shortening for anonymous single method objects. Its main
characteristics are:
Closure Definition To introduce a closure a special syntax is provided, without any
explicit reference to the object type. A closure definition (lambda expression) requires
specifying the closure argument names (if any), the generic types (if any) and the
closure body; arguments types are optional.
Type Inference The closure definition does not specify the type of the defined closure
and can omit argument types: The type system infers them all. In case of failure
during the inference process, a type error occurs.
SAM Types Interface types with a single method, named functional interfaces (SAM
types) are the types of the closures. As all Java reference types, functional interfaces
are nominal types, i.e they are different types if they have different names even
though they have the same structure. For this reason, a closure can be assigned to
(i.e. is compatible with) many different types.
Generic types Generics, specified in the closure definition, instantiate the generic vari-
ables defined in the single method signature of a suitable functional interface. A
problem arises: What is a suitable interface and what is its relation with the type
of the closure?
Target Types The solution adopted is to assign to a closure the target type, that is
the expected type in the specific context in which the closure is used. The target
type becomes the type if it is compatible with the closure.
Closure Contexts The possible contexts in which a closure can appear are:
1. Variable declaration
2. Assignment
3. Return statement
4. Array initializer
5. Method or constructor argument
6. Lambda expression body
7. Conditional expression
8. Cast expression
Type Compatibility The conditions which must hold for a closure to be compatible
with a type are: i) The type must be a functional interface: Let m be its single
method. ii) Number and types of the closure arguments must be the same as those
of m. iii) Return types of the closure and of m must be compatible. iv) Exceptions
thrown by the closure body must be allowed in the throws clause of m.
Closure Invocation There is no ad hoc syntax for closure invocation. The user has
to specify, hence know, the name of the single method of the functional interface.
Non-local Variables Any name used but not declared in the closure must be either
declared final or effectively final. The concept of effectively final variables, already
introduced in Java SE 7, is now broadened, to mitigate the restriction on variables
updating. An effectively final variable is a variable which is not declared final but
its value is not modified.
Variable Shadowing As for blocks the local variables or formal parameters of a clo-
sure cannot shadow already declared names.
Meaning of this The self reference this in a closure refers to the object whose
method is enclosing the closure definition and not to the defined closure (this
transparency), thus disallowing recursive definitions through this. To define a re-
cursive closure, it’s necessary to associate a name to the closure, for instance through
variable declaration and initialization or assignment.
The new features of this proposal are mainly concerned with (1) SAM types, (2)
target types and compatibility, (3) type inference of closure arguments. The challenge
here is to understand if a calculus with such features is actually type safe and in the latter
case which structures are necessary to provide a type safe semantics to closures. With
this aim, we use the same approach we adopted for studying the previous proposals. We
extend the calculus FGJ [IPW01] by defining a type system and a reduction semantics
for interfaces and anonymous classes, FGAJ [BO12], and for this kind of closures (here
called, Target Closure), obtaining the new calculus FGATCJ. Then, we prove the type
soundness.
Section 2 contains a brief presentation of the aims and the main features of FGJ.
Section 3 defines syntax and semantics of FGATCJ. Section 4 contains the main results
to prove type soundness. Section 5 contains a small example that sketches how the type
system is used to assign types to closures. Section 6 concludes the paper.
2 Featherweight Generic Java
A program in FGJ [IPW01] consists of a declaration of generic class definitions and of
an expression to be evaluated using the classes. The expression corresponds to the body
of the 0-arguments main method of ordinary Java.
A complete definition of the syntax of FGJ consists of the grammar rules in Table
1 that are labelled by the defined grammatical category indexed by FGJ. Symbols C
and ↑ are a notational shorthands for Java keyword extends and return. For syntactic
regularity, (a) classes always specify the super class, possibly Object, and have exactly
one constructor definition; (b) class constructors have one parameter for each class field
with the same name as the field, invoke the super constructor on the fields of the super
class and initialize the remaining fields to the corresponding parameters; (c) field access
always specifies the receiver (object), possibly this. This results in the stylized form of
the constructors. Both classes and methods may have generic type parameters.
FGJ has no side effects. Hence, sequencing and assignment are strictly confined to
constructor bodies. In particular, method bodies have always the form return, followed
by an expression. The lack of Java constructs for sequencing control and for store up-
dating (along with that of concurrency, and reflection) is the main advantage of the
calculus in studying language properties that are not affected by side effects. In this
way the calculus is, as much as possible, compact and takes advantage of the referential
transparency. The latter one provides a simple reduction semantics which is crucial for
rigorous, easy to derive, proofs of the language properties [FF87]. About compactness,
FGJ has only five forms of expressions (see definition of category e in Table 1): One
for variables1 , another for field access, and one for Object Creation. The remaining two
forms are method invocation and cast.
The presence of cast in FGJ is justified from its fundamental role in compiling generic
classes. We conclude this presentation considering the twofold role of referential trans-
parency: First, evaluation is entirely formalized within the syntax of FGJ (hence, the
evaluation process results in a sequence of FGJ expressions reducing the first one to
the last one, if any, which represents an error or its value) second, the order in which
expressions are reduced, if more than one can be selected, does not affect the final result.
The reduction semantics of FGJ consists of the first three rules that appear in Table
2: Computation, and deal with term evaluation, and of the first five rules in Table
2: Congruence, that deal with the redex selection. The remaining 20 rules of the se-
mantics of FGJ deal with the type system and with term well-formedness. The rules of
FGJ have labels that are indexed by FGJin Table 2, 4, 5.
3 Featherweight GATCJ
The calculus defined in this paper is obtained as an extension of the calculus FGAJ,
which is in turn an extension of FGJ, with interfaces, anonymous classes and conse-
quently objects from anonymous classes creation. FGATCJ extends FGAJ with the
closures defined in [BS11a]. About the non-local variables in closures, there is no mat-
ter since all the variables of FGJ can be considered effectively final. Similarly, about
variable shadowing, since FGJ programs are, in effect, abstract syntax terms.
3.1 Notation and General Conventions
In this paper we adopt the notation used in [IPW01], accordingly f is a shorthand for a
possibly empty sequence f1 , . . . , fn (and similarly for T, x, etc.) and M is a shorthand for
1
Variables, indicated with category x, include parameters and this. From a syntactic point
of view, this is a keyword in Java, and is a variable in FGJ but in both languages, it has
the meaning of object self-reference and allows method recusion, see rule GR-Invk, Table 2.
M1 . . . Mn (with no commas) where n is the size |f|, respectively |M|, i.e. the number of
terms of the sequence. The empty sequence is ◦ and symbol ”,” denotes concatenation
of sequences. Operations on pairs of sequences are abbreviated in the obvious way C f
is C1 f1 , . . . , Cn fn and similarly C f; is C1 f1 ; . . . Cn fn ; and this.f = f; is a shorthand
for this.f1 = f1 ; . . . this.fn = fn ; Sequences of field declarations, parameters and
method declaration cannot contain duplications. Cast, ( ) , and closure definition, → ,
have lower precedence than other operators, and cast precedes closure definition. Hence
() → (this.invoke()) can be written as () → this.invoke(). The, possibly indexed
and/or primed, metavariables T, V, U, S, W range over type expressions; T, X, Y, Z range
over type variables; N, P, Q range over class types; C, D, E range over class names; f, g
range over field names; e, v, d range over expressions; x, y range over variable names
and M, K, L and m range respectively, over methods, constructors, classes, and method
names. [x/y]e denotes the result of replacing y by x in e. Eventually F V (T) denotes the
set of free type variables in T.
3.2 Syntax
The syntax of FGATCJis reported in Table 1. Besides interface definition and anony-
mous classes already contained in FGAJand FGACJin [BO12], in FGATCJit is possible
to define closures through lambda expressions as proposed in [BS11a]2 . Accordingly, syn-
tax is extended only to construct a closure, for which two cases are considered: closures
with and without argument types. A further extension to expressions is concerned with
cast to interface type, which is maintained distinct from cast to class type, for technical
convenience.
Table 1 : Syntax
FGJ
T, V ::= X | N (TFGJ )
N ::= ChTi (NFGJ )
L ::= class ChX C Ni C N {T f; K M} (LFGJ )
K ::= C(T f){super(f); this.f = f; } (KFGJ )
M ::= hX C NiT m(T x){↑ e; } (MFGJ )
e ::= x | e.f | new N(e) | e.mhTi(e) | (N)e (eFGJ )
IA: Extensions for Interfaces and Anonymous Class Objects
T ::= IhTi (TFGAJ )
L ::= interface I hX C Ni{H} (LFGAJ )
H ::= hX C NiT m(T x) (HFGAJ )
e ::= new IhTi() {M} (eFGAJ )
TC: Extensions for Targeted Closures
e ::= a | (IhTi)e (eFGATCJ )
a ::= hVi(T x) → e | hVi(x) → e (aFGATCJ )
FGAJ = FGJ + IA
FGATCJ = FGJ + IA + TC
At the bottom of Table1, the syntactic structure of the various calculi, considered in
the paper, is resumed. For space convenience, the reduction rules of the semantics as
well as the typing rules are not given in separate tables for each calculus. In fact, since
compositionality of the semantics (we use), the rules of the various constructs are the
2
The concrete syntax adopted in the actual proposal in [BS11a] is different from the one
contained in Table 1 which is to be considered an abstract syntax
same in all calculi containing such a construct. However, for the reader convenience, in
all tables, but Table 3, the rules for each calculus, FGJ, FGAJ and FGATCJ, have
a label which is indexed by the name of the minimal calculus including the construct,
involved in the rule. Note that ChTi includes Object(since T may be the empty sequence
and C may be Object) hence generic variables in classes and methods can be instantiated
with types T that include interfaces.
3.3 Semantics: Reduction
Table 2: Computation
Computation
fields(N) = T f
(GR-FieldFGJ )
(new N(e)).fi ei
mbody(mhVi, N) = x.e
(GR-InvkFGJ )
(new N(e)).mhVi(d) [d/x, new N(e)/this]e
∅ ` N<:P
(GR-CastFGJ )
(P)(new N(e)) new N(e)
mbody(mhVi, new IhTi(){M}) = x.e
(GR-Invk-AnonymFGAJ )
(new IhTi(){M}).mhVi(d) [d/x, new IhTi(){M}/this]e
(hSi(T x) → e).mhSi(d) [d/x]e (GR-Clos-Inv-TypeFGATCJ )
(hSi(x) → e).mhSi(d) [d/x]e (GR-Clos-InvFGATCJ )
(IhTi) a a (GR-CCastFGATCJ )
Congruence
0
e0 e0
0 (GRC-FieldFGJ )
e0 .f e0 .f
0
e0 e0
0 (GRC-T-InvFGJ )
e0 .mhTi(e) e0 .mhTi(e)
0
ei ei
0 (GRC-Inv-ArgFGJ )
e0 .mhTi(. . . , ei , . . .) e0 .mhTi(. . . , ei . . .)
0
ei ei
0 (GRC-NewFGJ )
new N(. . . , ei , . . .) new N(. . . , ei , . . .)
0
e e
0 (GRC-CastFGJ )
(N)e (N)e
0
e e
0 (GRC-CCastFGATCJ )
(IhTi)e (IhTi)e
The reduction semantics is given through the inference rules in Table 2, which define
the reduction relation e e0 that says that “expression e reduces to expression e0 in
one step”. The set of expressions which cannot be further reduced is the set of normal
forms and constitute values of the calculus. In FGATCJ values are objects, constructed
out of anonymous or named classes, and of closures. Hence the grammatical category v
defines the syntactic form of the values of the calculus FGATCJ:
v ::= new N(v)
| new IhTi(){M}
| hSi(x) → e
| hSi(T x) → e
The structure of values results from the reduction rules of the calculus. The rules indexed
by FGJ in Table 2 are the same as those of calculus FGJ introduced in [IPW01], and
the one indexed by FGAJ is the same as those of the calculus FGAJ introduced in
[BO12], which include only one new rule, GR-Invk-AnonymFGAJ . This rule defines the
semantics of invocation with anonymous class objects, quite similar to the one of method
Table 3: Classes and Interfaces
Subclassing
CED DEE class ChX C Ni C D {S f; K M}
CEC
CEE CED
Auxiliary functions
fields(Object) = ◦ (F-Object)
class ChX C Ni C N {S f; K M} fields([T/X]N) = U g
(F-Class)
fields(ChTi) = U g, [T/X]S f
class ChX C Ni C N {S f; K M} hY C PiU m (U x){↑ e; } ∈ M
(MT-Class)
mtype(m, ChTi) = [T/X](hY C PiU 7→ U)
class ChX C Ni C N {S f; K M} m 6∈ M
(MT-Super)
mtype(m, ChTi) = mtype(m, [T/X]N)
interface IhX C Ni {H} hY C PiU m(U x) ∈ H
(MT-Interface)
mtype(m, IhTi) = [T/X](hY C PiU 7→ U)
class ChX C Ni C N {S f; K M} hY C PiU m (U x){↑ e; } ∈ M
(MB-Class)
mbody(mhVi, ChTi) = x.[T/X, V/Y]e
class ChX C Ni C N {S f; K M} m 6∈ M
(MB-Super)
mbody(mhVi, ChTi) = mbody(mhVi, [T/X]N)
interface IhX C Ni {...} hY C PiU m (U x){↑ e; } ∈ M
(MB-Interface)
mbody(mhVi, new IhTi(){M}) = x.[T/X, V/Y]e
interface IhX C Ni {H} |H| = 1 ∆ ` V<:[V/X]N hY C PiU m (U x) = H
(Method)
∆ ` met(IhVi) = hY C [V/X]Pi[V/X]U m ([V/X]U x)
Auxiliary predicates
override(m, Object, hY C PiT 7→ T0 ) (Over-Object)
mtype(m, N) = hZ C QiU 7→ U0 implies
((P, T) = [Y/Z](Q, U) and Y<:P ` T0 <:[Y/Z]U0 )
(Over)
override(m, N, hY C PiT 7→ T0 )
isClos(hVi(x) → e) (IsClosure)
isClos(hVi(T x) → e) (IsClosureTyped)
interface IhX C Ni {H} ∆ ` V<:[V/X]N |H| = 1
(Fun)
∆ ` Fun(IhVi)
DCast
dcast(C, D) dcast(D, E) class ChX C Ni C DhTi {. . .} X = F V (T)
(DCast)
dcast(C, E) dcast(C, D)
invocation with object of named classes. The new rules indexed FGATCJinclude method
invocation on closure values, which can be defined specifying arguments types or not,
and a rule to cast closures to interface types (targeting). Also one congruence rule for
casting is added. As a matter of fact, we could generalize FGJcasting rules but we prefer
here to maintain the division to point out semantics of the new constructs. Eventually,
note that no congruence rule has been added for closures this means that syntactically
different closures are different, in particular, hSi(T x) → e, hSi(T x) → e0 are different
values even though e e0 .
3.4 Semantics: Typing
The typing rules use three different kinds of environment, ∆ (for type variables), Γ
(for variables), and Ψ (for closures), and six different typing judgements: one for each
different term structure of the language. A (well formed) type environment ∆ is a
mapping from type variables to (well formed, in ∆) types written as a list of X<:T (with
at most one binding for each type variable X), meaning that type variable X must be
bound to a subtype of type T: ∆(X) = T if ∆ contains X<:T, undefined otherwise (i.e.
X∈/ dom(∆)). An environment Γ is a mapping from variables to types written as a list of
x : T (with at most one binding for each value variable x), meaning that “x has type T”.
An environment Ψ is a mapping from closure definitions to target (SAM) types written
as a list of a ⇓ T (with, at most, one binding for each closure a), meaning that closure
a has target type T. The judgement for a (generic) type T (see Table 5) has the form
∆ ` T ok meaning that “T is a well-formed type in the (well formed) type environment
∆”. The judgement for sub-typing (see Table 5) has the form ∆ ` S<:T meaning that
“S is a subtype of T in ∆”. The judgement for classes (see rule GT-ClassFGJ in Table
4b) has the form C OK meaning that “C is well typed”. The judgement for class methods
(see GT-MethodFGJ in Table 4b) has the form M OK IN C meaning that “M is well
typed when its declaration occurs in class C”. For methods in instances of anonymous
classes, the judgement is the same as for class methods but the inference has to consider
that these methods are defined in, runtime evaluated, interface instantiations, and they
must have the same signature that has been declared in the corresponding interfaces (see
GT-AnonymFGAJ in Table 4b). The judgement for expressions (see the rules of Table
4) has the form Ψ ; ∆; Γ ` e : T meaning that expression e has type T in the context of
environments Ψ , ∆ and Γ . The judgment for SAM types (see the rules of Table 4a) has
the form Ψ ; ∆; Γ ` a ↓ T meaning that closure a is compatible with SAM type T in the
context of environments Ψ , ∆ and Γ . The typing rules are contained in Table 4 and
extends those of FGJ [IPW01], and those of FGAJ [BO12], but relevant extensions have
been introduced: A new environment Ψ has been added to the (semantic) context of the
rules; the sixth judgment ↓ has been added, together with the corresponding inference
rules (of Table 4a), to deal with closure type compatibility.
Environment Ψ . The requirement for a third, additional, environment, Ψ , is one of
the most interesting and innovative aspect of the type system. In effect, as we noted
in Section 1, a closure has, possibly several, different, compatible SAM types in each
of the specific contexts in which it can occur in a program. Each compatible type of
a closure, in a context, can furnish a type to the closure, but the target type of the
context is actually chosen for typing the closure, provided it is one of the closure
compatible types.3 Hence, the environment Ψ is used to store, in each context of the
program, the binding of each closure, used in such a context, to its target.
3
This is an effect of the use of SAM types as the type closure domain of the calculus, and SAM
types are nominal types. In case of structural types, as functional types [BO12], a closure
should have only one compatible type and this type must be a supertype of the target type
Target, Compatible and Closure Type. Closure typing involves three different types.
The relation among such types is fully expressed by rule GT-ClosureFGATCJ, in Ta-
ble 4. The rule says that a closure a has type T in a context C ≡ Ψ ; ∆; Γ , if a is
an instance of a closure definition ac , i.e. a ≡ [d/x]ac for a terms substitution [d/x],
and in context C: ac has target type T, i.e. Ψ ≡ Ψ1 , ac ⇓ T and T is a compatible type
of ac .
Growth of Ψ . The combined use of compatible and target type leads to the definition
of inference rules, to assign types to closures, which appear a little strange in the way
they use the environment Ψ . All these rules have Ψ that increases in the conclusion
of the rule. This is the case of rules GT-InvFGJ , GT-NewFGJ , GT-ClosureFGAJ in
Table 4, of rules CompatibilityCBFGATCJ, CompatibilityTCBFGATCJ in Table
Table 4: Typing Rules
Ψ ; ∆; Γ1 , x : T, Γ2 ` x : T (GT-VarFGJ )
Ψ ; ∆; Γ ` e0 : T0 fields(bound∆ (T0 )) = T f
(GT-FieldFGJ )
Ψ ; ∆; Γ ` e0 .fi : Ti
mtype(m, bound∆ (T0 )) = hY C PiU 7→ U
Ψ ; ∆; Γ ` e0 : T0 ∆ ` V ok ∆ ` V<:[V/Y]P
isClos(ei ) Ψ ; ∆; Γ ` ei ↓ [V/Y]Ui
Ψ, ei ⇓[V/Y]Ui ; ∆; Γ ` e : S ∆ ` S<:[V/Y]U
(GT-InvFGJ )
Ψ, ei ⇓[V/Y]Ui ; ∆; Γ ` e0 .mhVi(e) : [V/Y]U
∆ ` N ok fields(N) = T f isClos(ei )
Ψ ; ∆; Γ ` ei ↓ Ti Ψ, ei ⇓Ti ; ∆; Γ ` e : S ∆ ` S<:T
(GT-NewFGJ )
Ψ, ei ⇓Ti ; ∆; Γ ` new N(e) : N
Ψ ; ∆; Γ ` e0 : T0 ∆ ` bound∆ (T0 )<:N
(GT-UCastFGJ )
Ψ ; ∆; Γ ` (N)e0 : N
Ψ ; ∆; Γ ` e0 : T0 ∆ ` N ok ∆ ` N <: bound∆ (T0 )
N = ChTi bound∆ (T0 ) = DhUi dcast(C, D)
(GT-DCastFGJ )
Ψ ; ∆; Γ ` (N)e0 : N
Ψ ; ∆; Γ ` e0 : T0 ∆ ` N ok
N = ChTi bound∆ (T0 ) = DhUi CE6 D 6 C
DE
(GT-SCastFGJ )
Ψ ; ∆; Γ ` (N)e0 : N
∆ ` IhTi ok Ψ ; ∆; Γ ` M OK IN IhTi
(GT-AnonymNewFGAJ )
Ψ ; ∆; Γ ` new IhTi(){M} : IhTi
Ψ ; ∆; Γ ` d : S ∆ ` S<:T Ψ ; ∆; Γ, x : T ` a ↓ T
(GT-ClosureFGATCJ )
Ψ, a⇓T; ∆; Γ ` [d/x]a : T
Ψ ; ∆; Γ ` a : IhTi
(GT-CCastFGATCJ )
Ψ ; ∆; Γ ` (IhTi)a : IhTi
4.a and of rule GT-AnonymCBFGAJ in Table 4.b. Ψ is extended only if the closure
is compatible with the target type.
Closure Contexts The typing rules of closures take into account the context in which
the closure appears in the program. In Section1 we recall that eight are the contexts
that JSR 000335 [BS11a,BS11b] admits for closures. The minimal core calculus
FGATCJreduces
Table 4a: Typing Rule - target compatibility
Closure compatibility
∆ ` T<:IhVi ∆ ` Fun(IhVi) isClos(e)
∆ ` met(IhVi) = hY C PiU m(S w) ∆ ` W<:[W/Y]P
Ψ ; ∆; Γ, x : [W/Y]S ` e ↓ [W/Y]U
(CompatibilityCBFGATCJ )
Ψ, e ⇓ [W/Y]U; ∆; Γ ` hWi(x) → e ↓ T
∆ ` T<:IhVi ∆ ` Fun(IhVi) ∼ isClos(e)
∆ ` met(IhVi) = hY C PiU m(S w) ∆ ` W<:[W/Y]P
Ψ ; ∆; Γ, x : [W/Y]S ` e : Z ∆ ` Z<:[W/Y]U
(CompatibilityFGATCJ )
Ψ ; ∆; Γ ` hWi(x) → e ↓ T
∆ ` T<:IhVi ∆ ` Fun(IhVi) isClos(e)
∆ ` met(IhVi) = hY C PiU m(S w) ∆ ` W<:[W/Y]P
∆ ` T<:[W/Y]S Ψ ; ∆; Γ, x : T ` e ↓ [W/Y]U
(CompatibilityTCBFGATCJ )
Ψ, e ⇓ [W/Y]U; ∆; Γ ` hWi(T x) → e ↓ T
∆ ` T<:IhVi ∆ ` Fun(IhVi) ∼ isClos(e)
∆ ` met(IhVi) = hY C PiU m(S w) ∆ ` W<:[W/Y]P
∆ ` T<:[W/Y]S Ψ ; ∆; Γ, x : T ` e : Z ∆ ` Z<:[W/Y]U
(CompatibilityTFGATCJ )
Ψ ; ∆; Γ ` hWi(T x) → e ↓ T
Table 4b: Typing Rules
Classes, Interfaces, Methods
∆ = X<:N, Y<:P ∆ ` T, T, P ok ∼ isClos(e0 )
∅; ∆; x : T, this : ChXi ` e0 : S ∆ ` S<:T
class ChX C Ni C N{...} override(m, N, hY C PiT 7→ T)
(GT-MethodFGJ )
hY C PiT m(T x){↑ e0 ; } OK IN ChX C Ni
∆ = X<:N, Y<:P ∆ ` T, T, P ok isClos(e0 )
∅; ∆; x : T, this : ChXi ` e0 ↓ T
class ChX C Ni C N{...} override(m, N, hY C PiT 7→ T)
(GT-MethodCBFGJ )
hY C PiT m(T x){↑ e0 ; } OK IN ChX C Ni
Y<:P, X<:N ` T, T, P ok
(GT-HeaderFGAJ )
hY C PiT m(T x) OK IN IhX C Ni
0 0
∆ = ∆, X<:N, Y<:P ∆ ` T, T, P ok ∼ isClos(e0 )
0 0
Ψ ; ∆ ; Γ, x : T, this : ChXi ` e0 : S ∆ ` V<:[V/X]N
0
∆ ` S<:T interface IhX C Ni{H} hY C PiT m(T x) ∈ H
(GT-AnonymFGAJ )
Ψ ; ∆; Γ ` hY C PiT m(T x){↑ e0 ; } OK IN IhVi
0 0
∆ = ∆, X<:N, Y<:P ∆ ` T, T, P ok isClos(e0 )
0 0
Ψ ; ∆ ; Γ, x : T, this : ChXi ` e0 ↓ T ∆ ` V<:[V/X]N
interface IhX C Ni{H} hY C PiT m(T x) ∈ H
(GT-AnonymCBFGATCJ )
Ψ, e0 ⇓ T; ∆; Γ ` hY C PiT m(T x){↑ e0 ; } OK IN IhVi
X <: N ` N, N, T ok M OK IN ChX C Ni
f ields(N) = U g K = C(U g, T f){super(g); this.f = f; }
(GT-ClassFGJ )
class ChX C Ni C N{T f; K M} OK
X <: N ` N ok H OK IN IhX C Ni
(GT-InterfFGAJ )
interface IhX C Ni{H} OK
Table 5: Subtypes
Subtypes
bound∆ (X) = ∆(X) (B-VarFGJ )
bound∆ (N) = N (B-ClassFGJ )
bound∆ (IhVi) = IhVi (B-InterfaceFGJ )
∆ ` T <: T (S-ReflFGJ )
∆ ` S <:T ∆ ` T<:U
(S-TransFGJ )
∆ ` S <: U
∆ ` X<:∆(X) (S-VarFGJ )
class ChX C Ni C N{. . .}
(S-ClassFGJ )
∆ ` ChTi <: [T/X]N
Well-formed types
∆ ` Object ok (WF-ObjectFGJ )
X ∈ dom(∆)
(WF-VarFGJ )
∆ ` X ok
class ChX C Ni C N{. . .} ∆ ` T ok ∆ ` T<:[T/X]N
(WF-ClassFGJ )
∆ ` ChTi ok
interface IhX C Ni{. . .} ∆ ` T ok ∆ ` T<:[T/X]N
(WF-InterfFGAJ )
∆ ` IhTi ok
them to the following four: 3. Return statement; 5. Method or constructor argu-
ment; 6. Lambda expression body; 8. Cast expression. Each of these contexts ex-
presses a target type for the closure that occurs in it. Hence the typing rules include
rules that check that such a type is one of the compatible types of the closure. In
particular, in Table 4, rule GT-InvFGJ deals also with closures that are argument
of method (i.e. context 5). Rule GT-NewFGJ deals also with closures that are argu-
ment of constructor (i.e. context 5). In Table 4.a, rules CompatibilityCBFGATCJ
and CompatibilityTCBFGATCJ deal with closures that are the body of another clo-
sure (i.e. context 7). In Table 4.b, rule GT-MethodCBFGJ deals with closures that
are the return expression of a method (i.e. context 3). Rule GT-AnonymCBFGATCJ
deals with closures that are the return expression of an interface instance method
(i.e. context 3).
4 Properties
Semantics is useful to prove language properties. In this paper we consider the sound-
ness of the type system for closures with SAM types. Analogously to [IPW01], we prove
the subject reduction theorem and the progress theorem first, the type soundness im-
mediately follows. For space problems, we give the statements of all the three but only
a sketched proof of the first two theorems. Several interesting lemmas are used in the
complete theorem proofs, we omit them at all, but we give the statements of two lemmas
that are used in the sketched proofs.
Theorem 1 (Subject reduction). If Ψ ; ∆; Γ ` e : T and e e0 then Ψ ; ∆; Γ ` e0 : T0 ,
for some T0 such that ∆ ` T0 <:T
Proof. By induction on the reduction e e0 , with a case analysis on the reduction
rule used. The proof of the corresponding theorem for FGJ (pp. 426-428, [IPW01]),
must be extended with the following cases GR-Clos-Inv, GR-Clos-Inv-Type and
GR-CCast. The first two are quite similar, the third one is trivial. We show GR-
Clos-Inv: e = hSi(x) → eb .mhVi(e) e0 = [e/x]eb By rule GT-Inv
(1)
Ψ ≡ Ψ1 , ei ⇓ [V/Y]Ui Ψ1 ; ∆; Γ ` hSi(x) → eb : Ta ∆ ` V<:[V/Y]P
mtype(m, bound∆ (Ta )) = hY C Pi U → U ∆ ` V ok isClos(ei )
Ψ1 ; ∆, Γ ` ei ↓ [V/Y]Ui Ψ1 ; ∆; Γ ` e : T ∆ ` T<:[V/Y]U T ≡ [V/Y]U
From (1), by GT-Closure, (2) Ψ2 ; ∆; Γe ` ec ↓ Ta for Ψ1 = Ψ2 , ec ⇓ Ta and Γe ≡ Γ, y : Ty
and (3) [d/y]ec ≡ hSi(x) → eb . From (2), by Lemma 3 we have Ψ2 ; ∆; Γ ` [d/x]ec ↓ Ta
and since (3), Ψ2 ; ∆; Γ ` hSi(x) → eb ↓ Ta . We should consider the other three rules in
Table 4a, but we consider only the case ∼ isClos(eb ). By Compatibility
∆ ` Ta <:Ia hVa i ∆ ` met(Ia hVa i) = hY C Pi U m(U w)
(4)
∆ ` Fun(Ia (Va )) Ψ2 ; ∆; Γ, x : [V/Y]U ` eb : Z ∆ ` Z<:[V/Y]U
From (4), by Lemma 2, Ψ2 ; ∆; Γ ` [e/x]eb : Z0 for ∆ ` Z0 <:Z and by S-Trans, ∆ `
Z0 <:[V/Y]U. Eventually by Lemma 1, Ψ ; ∆; Γ ` [e/x]eb : Z0 . Letting T0 = Z0 finishes the
case.
Theorem 2 (Progress). Suppose e is well-type. If e includes as a subexpression:
1. new N(e).f then f ields(N) = T f, for some T and f, and f ∈ f.
2. new N(e).mhVi(d) then mbody(mhVi, N) = x.e0 , for some x and e0 , and |x| = |d|.
3. (hSi(T x) → e0 ).mhSi(d) then |x| = |d| = |T| for some T, x and e0 .
4. (hSi(x) → e0 ).mhSi(d) then |x| = |d| for some x and e0 .
Proof. The proof is based on the analysis of all well typed expressions, which can be
reduced to the above 4 cases, to conclude that either it is in normal form or it can be
further reduced to obtain a normal form (see section 3.3)
∗
Theorem 3 (Type Soundness). If Ψ ; ∅; ∅ ` e : T and e e0 with e0 a normal form,
then e0 is a value v with Ψ ; ∅; ∅ ` v : S and ∅ ` S<:T
Lemma 1. Suppose ∆, X<:N ` N ok and ∆ ` T, T ok
1. If ∆ ` S<:T, then ∆, X<:N ` S<:T
2. If ∆ ` S ok, then ∆, X<:N ` S ok
3. If Ψ ; ∆; Γ ` e : T, then Ψ ; ∆; Γ, x : T ` e : T and Ψ ; ∆, X<:N; Γ ` e : T and
Ψ, e ⇓ T; ∆; Γ ` e : T
Lemma 2. If Ψ ; ∆; Γ, x : T ` e : T and Ψ ; ∆; Γ ` d : S where ∆ ` S<:T, then Ψ ; ∆; Γ `
[d/x]e : S for some S such that ∆ ` S<:T
Lemma 3. Let e ≡ hWi(x) → eb or e ≡ hWi(T x) → eb . If Ψ ; ∆; Γ, y : Ty ` e ↓ T and
Ψ ; ∆; Γ ` d : Sy for ∆ ` Sy <:Ty then Ψ ; ∆; Γ ` [d/y]e ↓ T
5 Example
Consider a program with a class Integer (whose definition is omitted, with two object:
2 and 3) and three interfaces that define three SAM types. In particular, I0 and I2
introduce two different SAM types and are such that for each closure a (and any context
Ψ ; ∆; Γ ) we have (Ψ ; ∆; Γ `)a ↓ I0 if and only if (Ψ ; ∆; Γ `)a ↓ I2 . This is due to the
nominal nature of the SAM types.
interface I0 {Integer invoke()}; interface I1 {I0 invoke(Integer x)};
interface I2 {Integer invoke()}
Consider the following expression, ((I1 )((x) → () → 3)).invoke(2), and if and how a
(unique) type can be assigned to it. We use the type system to show that a (principal)
type T and an environment Ψ exist: Ψ ; ∅; ∅ ` ((I1 )((x) → () → 3)).invoke(2) : T.
The computation is sketched below.
Ψ ; ∅; ∅ ` ((I1 )((x) → () → 3)).invoke(2) : T by GT-Inv
e0 = (I1 )((x) → () → 3) T = I1
Ψ ; ∅; ∅ ` (I1 )((x) → () → 3) : I1 by GT-CCast
Ψ ; ∅; ∅ ` (x) → () → 3 : I1 by GT-Closure
d≡x Γ ≡∅
Ψ1 ; ∅; ∅ ` (x) → () → 3 ↓ I1 by CompatibilityCB
∅ ` I1 <:I1 isClos(() → 3) ∅ ` Fun(I)
∅ ` met(I1 ) = I0 invoke(Integer x)
Ψ2 , ∅; ∅; ` () → 3 ↓ I0 by Compatibility
∅ ` I0 <:I0 ∼ isClos(3) ∅ ` Fun(I0 )
∅ ` met(I0 ) = Integer invoke()
Ψ2 , ∅; ∅; ` 3 : Integer
Ψ1 = Ψ2 , () → 3 ⇓ I0 Ψ2 = ∅
Ψ = Ψ1 , (x) → () → 3 ⇓ I1
mtype(invoke, I1 ) = Integer → I0
Ψ ; ∅; ∅ ` 2 : Integer
Ψ ; ∅; ∅ ` (I1 )((x) → () → 3).invoke(2) : I0
Hence Ψ = (x) → () → 3 ⇓ I1 , () → 3 ⇓ I0 , e reduces to () → 3 and
(x) → () → 3 ⇓ I1 , () → 3 ⇓ I0 ; ∅; ∅ ` () → 3 : I0
6 Conclusions
We have provided a type system and a reduction semantics for closures with SAM types
and type inference on closures and closure arguments [BS11a]. We proved the soundness
of the type system. This shows that we can use nominal types instead of structural,
functional types. The resulting system however, is not so easy if compared to the one
defined for simple closure [BO12].
References
[BLB06] D. Lea B. Lee and J. Bloch. Concise Instance Creation Expressions: Closure without
Complexity, 2006. crazybob.org/2006/10/java-closure-spectrum.html.
[BO11] M. Bellia and M.E. Occhiuto. Java in Academia and Research, chapter JavaΩ: Higher
Order Programming in Java, pages 166–185. iConcept Press Ltd., 2011.
[BO12] M. Bellia and M.E. Occhiuto. The equivalence of Reduction and Translation Semantics
of Java Simple Closures. Fundamenta Informaticae, 119:1–16, 2012.
[BS11a] A. Buckley and D. Smith. JSR-000335 Lambda Expressions for the Java Programming
Language - Early Draft Review: Lambda Specification, Version 0.4.2. Oracle Corpo-
ration, December 2011. http://download.oracle.com/otndocs/jcp/lambda-0 4 2-edr-
spec/index.html.
[BS11b] A. Buckley and D. Smith. State of the Lambda. Oracle Corporation, December 2011.
http://cr.openjdk.java.net/b̃riangoetz/lambda/lambda-state-4.html.
[FF87] Matthias Felleisen and Daniel P. Friedman. A Reduction Semantics for Imperative
Higher-Order Languages. In PARLE (2), pages 206–223, 1987.
[IPW01] A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java: A Minimal Core Calculus
for Java and GJ. ACM TOPLAS, 23:396–450, 2001.
[Ope12] OpenJDK. Project lambda, 2012. http://openjdk.java.net/projects/lambda/.