The paper presents FJ&λ, a new core calculus that extends Featherweight Java (FJ) with interfaces, supporting multiple inheritance in a restricted form, λ-expressions, and intersection types. The goal is to formalise how lambdas and intersection types are grafted on Java 8, by studying their properties in a formal setting. The authors show how intersection types play a significant role in several cases, in particular in the typecast of a λ-expression and in the typing of conditional expressions. We also embody interface emph{default methods} in FJ&λ, since they increase the dynamism of λ-expressions, by allowing these methods to be called on λ-expressions. The crucial point in Java 8 and in our calculus is that λ-expressions can have various types according to the context requirements (target types): indeed, Java code does not compile when λ-expressions come without target types. In particular, in the operational semantics we must record target types by decorating λ-expressions, otherwise they would be lost in the runtime expressions. The paper proves the subject reduction property and progress for the resulting calculus, and gives a type inference algorithm that returns the type of a given program if it is well typed. The design of FJ&λ has been driven by the aim of making it a subset of Java 8, while preserving the elegance and compactness of FJ. Indeed, FJ&λ programs are typed and behave the same as Java programs.
Java & Lambda: a Featherweight Story / Bettini, Lorenzo; Bono, Viviana ; Dezani-Ciancaglini, Mariangiola ; Giannini, Paola ; Venneri, Betti. - In: LOGICAL METHODS IN COMPUTER SCIENCE. - ISSN 1860-5974. - STAMPA. - 14:(2018), pp. 1-24. [10.23638/LMCS-14(3:17)2018]
Java & Lambda: a Featherweight Story
Bettini, Lorenzo;Venneri, Betti
2018
Abstract
The paper presents FJ&λ, a new core calculus that extends Featherweight Java (FJ) with interfaces, supporting multiple inheritance in a restricted form, λ-expressions, and intersection types. The goal is to formalise how lambdas and intersection types are grafted on Java 8, by studying their properties in a formal setting. The authors show how intersection types play a significant role in several cases, in particular in the typecast of a λ-expression and in the typing of conditional expressions. We also embody interface emph{default methods} in FJ&λ, since they increase the dynamism of λ-expressions, by allowing these methods to be called on λ-expressions. The crucial point in Java 8 and in our calculus is that λ-expressions can have various types according to the context requirements (target types): indeed, Java code does not compile when λ-expressions come without target types. In particular, in the operational semantics we must record target types by decorating λ-expressions, otherwise they would be lost in the runtime expressions. The paper proves the subject reduction property and progress for the resulting calculus, and gives a type inference algorithm that returns the type of a given program if it is well typed. The design of FJ&λ has been driven by the aim of making it a subset of Java 8, while preserving the elegance and compactness of FJ. Indeed, FJ&λ programs are typed and behave the same as Java programs.File | Dimensione | Formato | |
---|---|---|---|
Java Lambda.pdf
accesso aperto
Tipologia:
Pdf editoriale (Version of record)
Licenza:
Open Access
Dimensione
563.85 kB
Formato
Adobe PDF
|
563.85 kB | Adobe PDF |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.