From d2f58b24899108b5fc660cc9694aa12887c7addf Mon Sep 17 00:00:00 2001 From: Peter Thiemann Date: Tue, 28 May 2024 18:21:37 +0200 Subject: [PATCH] intro --- .gitignore | 4 ++++ TIforWildFJ.tex | 34 ++++++++++++++++----------- introduction.tex | 60 +++++++++++++++++++++++++++++++++++++----------- 3 files changed, 71 insertions(+), 27 deletions(-) diff --git a/.gitignore b/.gitignore index 35777cd..bde021f 100644 --- a/.gitignore +++ b/.gitignore @@ -17,3 +17,7 @@ *-blx.aux *-blx.bib *.run.xml +*.vtc +*.synctex.gz +auto +_region_.tex diff --git a/TIforWildFJ.tex b/TIforWildFJ.tex index ea3a0b7..c83103d 100644 --- a/TIforWildFJ.tex +++ b/TIforWildFJ.tex @@ -1,5 +1,5 @@ -\documentclass{llncs} +\documentclass[anonymous,USenglish]{llncs} %This is a template for producing LIPIcs articles. %See lipics-v2021-authors-guidelines.pdf for further information. %for A4 paper format use option "a4paper", for US-letter use option "letterpaper" @@ -45,21 +45,19 @@ \title{Global Type Inference for Featherweight Java with Wildcards} %TODO Please add -%\titlerunning{Dummy short title} %TODO optional, please use if title is longer than one line +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% ANON -\author{Andreas Stadelmeier\inst{1}, Martin Plümicke\inst{1}, Peter Thiemann\inst{2}}%TODO mandatory, please use full name; only 1 author per \author macro; first two parameters are mandatory, other parameters can be empty. Please provide at least the name of the affiliation and the country. The full address is optional. Use additional curly braces to indicate the correct name splitting when the last name consists of multiple name parts. -\institute{DHBW Stuttgart, Campus Horb, Germany\\ -\email{a.stadelmeier@hb.dhbw-stuttgart.de} \and -Universität Freiburg, Institut für Informatik, Germany\\ -\email{thiemann@informatik.uni-freiburg.de}} +% \author{Andreas Stadelmeier\inst{1}, Martin Plümicke\inst{1}, Peter Thiemann\inst{2}} +% \institute{DHBW Stuttgart, Campus Horb, Germany\\ +% \email{a.stadelmeier@hb.dhbw-stuttgart.de} \and +% Universität Freiburg, Institut für Informatik, Germany\\ +% \email{thiemann@informatik.uni-freiburg.de}} -\authorrunning{A. Stadelmeier and M. Plümicke and P. Thiemann} %TODO mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et al.' - -%\Copyright{Andreas Stadelmeier and Martin Plümicke and Peter Thiemann} %TODO mandatory, please use full first names. LIPIcs license is "CC-BY"; http://creativecommons.org/licenses/by/3.0/ - -%\ccsdesc[500]{Software and its engineering~Language features} -%\ccsdesc[300]{Software and its engineering~Syntax} +% \authorrunning{A. Stadelmeier and M. Plümicke and P. Thiemann} +%% END ANON +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %\category{} %optional, e.g. invited paper @@ -96,7 +94,15 @@ Universität Freiburg, Institut für Informatik, Germany\\ %TODO mandatory: add short abstract of the document \begin{abstract} -TODO: Abstract + Type inference is a hallmark of functional programming. Its use in + object-oriented programming is often restricted to type inference + for local variables and the instantiation of generic type + parameters. + + Global type inference for Featherweight Generic Java is a + whole-program analysis that infers omitted method signatures. + Compared to previous work, its results are more general as it infers + types with wildcards. Global type inference is proved sound. \end{abstract} \keywords{type inference, Java, subtyping, generics} %TODO mandatory; please add comma-separated list of keywords diff --git a/introduction.tex b/introduction.tex index f689f3f..cba07d4 100644 --- a/introduction.tex +++ b/introduction.tex @@ -26,23 +26,52 @@ % It's only restriction is that no polymorphic recursion is allowed. % \end{recap} -\section{Type Inference for Java} -- Type inference helps rapid development -- used in Java already (var keyword) -- keeps source code clean +\section{Introduction} +\label{sec:introduction} -Java comes with a local type inference algorithm -used for lambda expressions, method calls, and the \texttt{var} keyword. +Type inference is a hallmark of functional programming, where it +improves readability and conciseness while +enabling safe rapid prototyping by allowing the compiler to deduce +types automatically without explicit type annotations. It allows +developers to safely refactor their programs before fixing function +signatures. In object-oriented programming (OOP), however, the use of +type inference is more restricted. It is often employed for local +variables and the instantiation of generic type parameters, offering +similar readability and conciseness benefits as in functional +programming. In languages like Java, the overall architecture of +method signatures must be designed by the programmer up-front. -A type inference algorithm that is able to recreate any type annotation -even when no type information is given at all is called a global type inference algorithm. -The global type inference algorithm presented here is able to deal with all Java types including wildcard types. -It can also be used for regular Java programs. +Java features a limited form of local type inference for local +variables defined with the \texttt{var} keyword, lambda expressions, +and method calls. Java infers the type of variables defined with +\texttt{var}. The rationale here is that instantiations of generic +types (e.g., maps of maps) are often unwiedly and they can be easily +inferred from the initializing expression. The type of a lambda +expression is inferred from the target type, i.e., the type of the +method argument that accepts the lambda. The rationale is the intended +use of lambdas as callback functions for listeners etc. For calls +to generic methods, Java infers the most specific instantiation of the +generic parameters for each individual call. + +The local type inference features of Java add some convenience, but +programmers still have to provide method signatures beforehand. So there +is scope for a global type inference algorithm that infers +method signatures even if no type information (except class headers +and types of field variables) is given. +We present such a global type inference algorithm for Featherweight +Generic Java with wildcards. The same approach can also be used for +regular Java programs. %The goal is to find a correct typing for a given Java program. -Type inference for Java has many use cases and could be used to help programmers by inserting correct types for them, -finding better type solutions for already typed Java programs (for example more generical ones), -or allowing to write typeless Java code which is then type inferred and thereby type checked by our algorithm. +Our algorithm enables programmers to write Java code with only a +minimum of type annotations (class headers and types of field +variables), it can fill in missing type annotations in partially +type-annotated programs, and it can suggest better (more general) +types for ordinary, typed Java programs. + + +\textbf{TO BE CONTINUED} + We propose a global type inference algorithm for Java supporting Wildcards and proven sound. Global type inference allows input programs without any type annotations. @@ -633,3 +662,8 @@ $\ntv{z}$ is a normal placeholder and is not allowed to contain free variables. \end{enumerate} %TODO: Move this part. or move the third challenge some underneath. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "TIforWildFJ" +%%% End: