This commit is contained in:
Peter Thiemann 2024-05-28 18:21:37 +02:00
parent c714d49677
commit d2f58b2489
3 changed files with 71 additions and 27 deletions

4
.gitignore vendored
View File

@ -17,3 +17,7 @@
*-blx.aux *-blx.aux
*-blx.bib *-blx.bib
*.run.xml *.run.xml
*.vtc
*.synctex.gz
auto
_region_.tex

View File

@ -1,5 +1,5 @@
\documentclass{llncs} \documentclass[anonymous,USenglish]{llncs}
%This is a template for producing LIPIcs articles. %This is a template for producing LIPIcs articles.
%See lipics-v2021-authors-guidelines.pdf for further information. %See lipics-v2021-authors-guidelines.pdf for further information.
%for A4 paper format use option "a4paper", for US-letter use option "letterpaper" %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 \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. % \author{Andreas Stadelmeier\inst{1}, Martin Plümicke\inst{1}, Peter Thiemann\inst{2}}
\institute{DHBW Stuttgart, Campus Horb, Germany\\ % \institute{DHBW Stuttgart, Campus Horb, Germany\\
\email{a.stadelmeier@hb.dhbw-stuttgart.de} \and % \email{a.stadelmeier@hb.dhbw-stuttgart.de} \and
Universität Freiburg, Institut für Informatik, Germany\\ % Universität Freiburg, Institut für Informatik, Germany\\
\email{thiemann@informatik.uni-freiburg.de}} % \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.' % \authorrunning{A. Stadelmeier and M. Plümicke and P. Thiemann}
%\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}
%% END ANON
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\category{} %optional, e.g. invited paper %\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 %TODO mandatory: add short abstract of the document
\begin{abstract} \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} \end{abstract}
\keywords{type inference, Java, subtyping, generics} %TODO mandatory; please add comma-separated list of keywords \keywords{type inference, Java, subtyping, generics} %TODO mandatory; please add comma-separated list of keywords

View File

@ -26,23 +26,52 @@
% It's only restriction is that no polymorphic recursion is allowed. % It's only restriction is that no polymorphic recursion is allowed.
% \end{recap} % \end{recap}
\section{Type Inference for Java} \section{Introduction}
- Type inference helps rapid development \label{sec:introduction}
- used in Java already (var keyword)
- keeps source code clean
Java comes with a local type inference algorithm Type inference is a hallmark of functional programming, where it
used for lambda expressions, method calls, and the \texttt{var} keyword. 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 Java features a limited form of local type inference for local
even when no type information is given at all is called a global type inference algorithm. variables defined with the \texttt{var} keyword, lambda expressions,
The global type inference algorithm presented here is able to deal with all Java types including wildcard types. and method calls. Java infers the type of variables defined with
It can also be used for regular Java programs. \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. %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, Our algorithm enables programmers to write Java code with only a
finding better type solutions for already typed Java programs (for example more generical ones), minimum of type annotations (class headers and types of field
or allowing to write typeless Java code which is then type inferred and thereby type checked by our algorithm. 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. We propose a global type inference algorithm for Java supporting Wildcards and proven sound.
Global type inference allows input programs without any type annotations. 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} \end{enumerate}
%TODO: Move this part. or move the third challenge some underneath. %TODO: Move this part. or move the third challenge some underneath.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "TIforWildFJ"
%%% End: