In this paper we consider the new type structure that has been proposed for Java closures, in the last Java Speci cation Language [BS11a]. This structure uses SAM types that are in fact, nominal types instead of the structural, functional types, used in the previous, proposals. In addition, it allows type inference for closures and for closure arguments. Through a technique, already 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 de ne 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]. Eventually, we prove the soundness of the type system.
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 De nition To introduce a closure a special syntax is provided, without any explicit reference to the object type. A closure de nition (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 de nition does not specify the type of the de ned 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 di erent types if they have di erent names even though they have the same structure. For this reason, a closure can be assigned to (i.e. is compatible with) many di erent types.
Generic types Generics, speci ed in the closure de nition, instantiate the generic variables de ned 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 speci c 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 e ectively nal. The concept of e ectively nal variables, already introduced in Java SE 7, is now broadened, to mitigate the restriction on variables updating. An e ectively nal variable is a variable which is not declared nal but its value is not modi ed.
Variable Shadowing As for blocks the local variables or formal parameters of a closure 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 de nition and not to the de ned closure (this transparency), thus disallowing recursive de nitions through this. To de ne a recursive 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 de ning 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 de nes 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
A program in FGJ [IPW01] consists of a declaration of generic class de nitions 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 de nition of the syntax of FGJ consists of the grammar rules in Table 1 that are labelled by the de ned 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 de nition; (b) class constructors have one parameter for each class eld with the same name as the eld, invoke the super constructor on the elds of the super class and initialize the remaining elds to the corresponding parameters; (c) eld access always speci es 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 e ects. Hence, sequencing and assignment are strictly con ned 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 updating (along with that of concurrency, and re ection) is the main advantage of the calculus in studying language properties that are not a ected by side e ects. 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 ve forms of expressions (see de nition of category e in Table 1): One for variables1, another for eld access, and one for Object Creation. The remaining two forms are method invocation and cast.
The presence of cast in FGJ is justi ed from its fundamental role in compiling generic classes. We conclude this presentation considering the twofold role of referential transparency: First, evaluation is entirely formalized within the syntax of FGJ (hence, the evaluation process results in a sequence of FGJ expressions reducing the rst 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 a ect the nal result. The reduction semantics of FGJ consists of the rst three rules that appear in Table 2: Computation, and deal with term evaluation, and of the rst ve rules in Table 2: Congruence, that deal with the redex selection. The remaining 20 rules of the semantics 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
The calculus de ned 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 consequently objects from anonymous classes creation. FGATCJ extends FGAJ with the closures de ned in [BS11a]. About the non-local variables in closures, there is no matter since all the variables of FGJ can be considered e ectively nal. Similarly, about variable shadowing, since FGJ programs are, in e ect, abstract syntax terms. 3.1
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 jfj, respectively jMj, 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 eld declarations, parameters and method declaration cannot contain duplications. Cast, ( ) , and closure de nition, ! , have lower precedence than other operators, and cast precedes closure de nition. 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 eld 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
The syntax of FGATCJis reported in Table 1. Besides interface de nition and anonymous classes already contained in FGAJand FGACJin [BO12], in FGATCJit is possible to de ne closures through lambda expressions as proposed in [BS11a]2. Accordingly, syntax 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. 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 di erent from the one contained in Table 1 which is to be considered an abstract syntax
FGJ T; V ::= X j N N ::= C T
h i L ::= class ChX C Ni C N fT f; K Mg K ::= C(T f)fsuper(f); this:f = f; g M ::= hX C NiT m(T x)f" e; g e ::= x j e:f j new N(e) j e:mhTi(e) j (N)e T ::= I T
h i L ::= interface I hX C NifHg H ::= hX C NiT m(T x) e ::= new IhTi() fMg TC: Extensions for Targeted Closures e ::= a j (IhTi)e a ::= hVi(T x) ! e j hVi(x) ! e FGAJ = FGJ + IA FGATCJ = FGJ + IA + TC IA: Extensions for Interfaces and Anonymous Class Objects (TFGJ) (NFGJ) (LFGJ) (KFGJ) (MFGJ) (eFGJ) (TFGAJ) (LFGAJ) (HFGAJ) (eFGAJ) (eFGATCJ) (aFGATCJ) 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
Computation
The reduction semantics is given through the inference rules in Table 2, which de ne 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 de nes the syntactic form of the values of the calculus FGATCJ: v ::= new N(v) j new IhTi()fMg j hSi(x) ! e j 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 de nes the semantics of invocation with anonymous class objects, quite similar to the one of method invocation with object of named classes. The new rules indexed FGATCJinclude method invocation on closure values, which can be de ned 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 di erent closures are di erent, in particular, hSi(T x) ! e, hSi(T x) ! e0 are di erent values even though e e0. 3.4
The typing rules use three di erent kinds of environment, (for type variables), (for variables), and (for closures), and six di erent typing judgements: one for each di erent 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, unde ned otherwise (i.e. X 2= 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 de nitions 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 de ned 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 e ect, as we noted in Section 1, a closure has, possibly several, di erent, compatible SAM types in each of the speci c 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 e ect 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 di erent types.
The relation among such types is fully expressed by rule GT-ClosureFGATCJ, in Table 4. The rule says that a closure a has type T in a context C ; ; , if a is an instance of a closure de nition 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 de nition 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 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 0 = ; X<:N; Y<:P 0 ` T; T; P ok isClos(e0)
; 0; ; x : T; this : ChXi ` e0 : S 0 ` V<:[V=X]N 0 ` S<:T interface IhX C NifHg hY C PiT m(T x) 2 H
; ; ` hY C PiT m(T x)f" e0; g OKIN IhVi 0 = ; X<:N; Y<:P 0 ` T; T; P ok isClos(e0) ; 0; ; x : T; this : ChXi ` e0 # T 0 ` V<:[V=X]N interface IhX C NifHg hY C PiT m(T x) 2 H ; e0 + T; ; ` hY C PiT m(T x)f" e0; g OKIN IhVi
X <: N ` N; N; T ok M OKIN ChX C Ni fields(N) = U g K = C(U g; T f)fsuper(g); this:f = f; g class ChX C Ni C NfT f; K Mg OK X <: N ` N ok H OKIN IhX C Ni interface IhX C NifHg OK (CompatibilityCBFGATCJ)
(CompatibilityFGATCJ) (CompatibilityTCBFGATCJ) (CompatibilityTFGATCJ)
(GT-MethodFGJ) (GT-MethodCBFGJ) (GT-HeaderFGAJ) (GT-AnonymFGAJ) (GT-AnonymCBFGATCJ)
(GT-ClassFGJ) (GT-InterfFGAJ) Subtypes them to the following four: 3. Return statement; 5. Method or constructor argument; 6. Lambda expression body; 8. Cast expression. Each of these contexts expresses 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 argument of constructor (i.e. context 5). In Table 4.a, rules CompatibilityCBFGATCJ and CompatibilityTCBFGATCJ deal with closures that are the body of another closure (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
Semantics is useful to prove language properties. In this paper we consider the soundness of the type system for closures with SAM types. Analogously to [IPW01], we prove the subject reduction theorem and the progress theorem rst, the type soundness immediately follows. For space problems, we give the statements of all the three but only a sketched proof of the rst 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.
for some T0 such that ` T0<:T ` e : T and e e0 then ; ; ` e0 : T0, 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 rst two are quite similar, the third one is trivial. We show GRClos-Inv: e = hSi(x) ! eb:mhVi(e) e0 = [e=x]eb By rule GT-Inv
1; ei + [V=Y]Ui (1) 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<:IahVai ` met(IahVai) = hY C Pi U m(U w) ` Fun(Ia(Va)) (4) 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 nishes 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 2 f. 2. new N(e):mhVi(d) then mbody(mhVi; N) = x:e0, for some x and e0, and jxj = jdj. 3. (hSi(T x) ! e0):mhSi(d) then jxj = jdj = jTj for some T, x and e0.
4. (hSi(x) ! e0):mhSi(d) then jxj = jdj 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 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; ; ` e : T Lemma 2. If ; ; ; x : T ` e : T and ; ; [d=x]e : S for some S such that ` S<:T ` d : S where ` S<:T, then ; ; `
; ; ` d : Sy for hWi(x) ! eb or e hWi(T x) ! eb. If ; ; ; y : Ty ` e # T and ` Sy<:Ty then ; ; ` [d=y]e # T 5
Consider a program with a class Integer (whose de nition is omitted, with two object: 2 and 3) and three interfaces that de ne three SAM types. In particular, I0 and I2 introduce two di erent 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. e0 with e0 a normal form, ` e : T and interface I0fInteger invoke()g; interface I1fI0 invoke(Integer x)g; interface I2fInteger invoke()g 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 ; ` I1<:I1 isClos(() ! 3) ; ` 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 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 de ned for simple closure [BO12].