TY - JOUR
T1 - Java & lambda
T2 - A featherweight story
AU - Bettini, Lorenzo
AU - Bono, Viviana
AU - Dezani-Ciancaglini, Mariangiola
AU - Giannini, Paola
AU - Venneri, Betti
N1 - Publisher Copyright:
© JAVA & LAMBDA: A FEATHERWEIGHT STORY.
PY - 2018/9/5
Y1 - 2018/9/5
N2 - We present FJ&λ, a new core calculus that extends Featherweight Java (FJ) with interfaces, supporting multiple inheritance in a restricted form, λ-expressions, and intersection types. Our main goal is to formalise how lambdas and intersection types are grafted on Java 8, by studying their properties in a formal setting. We 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 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. We prove the subject reduction property and progress for the resulting calculus, and we give 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.
AB - We present FJ&λ, a new core calculus that extends Featherweight Java (FJ) with interfaces, supporting multiple inheritance in a restricted form, λ-expressions, and intersection types. Our main goal is to formalise how lambdas and intersection types are grafted on Java 8, by studying their properties in a formal setting. We 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 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. We prove the subject reduction property and progress for the resulting calculus, and we give 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.
UR - http://www.scopus.com/inward/record.url?scp=85055823251&partnerID=8YFLogxK
U2 - 10.23638/LMCS-14(3:17)2018
DO - 10.23638/LMCS-14(3:17)2018
M3 - Article
SN - 1860-5974
VL - 14
JO - Logical Methods in Computer Science
JF - Logical Methods in Computer Science
IS - 3
M1 - 17
ER -