77 lines
4.3 KiB
TeX
77 lines
4.3 KiB
TeX
|
|
\section{Related Work}
|
|
Igarashi et al \cite{FJ} define Featherweight Java
|
|
and its generic sibling, Featherweight Generic Java. Their language is
|
|
a functional calculus reduced to the bare essentials, they develop the full metatheory, they
|
|
support generics, and study the type erasing transformation used by
|
|
the Java compiler. Stadelmeier et. al. extends this approach by global type
|
|
inference \cite{TIforFGJ}.
|
|
|
|
\subsection{Wildcards in formal Java models}
|
|
Wildcards are first described in a research paper in \cite{addingWildcardsToJava}. In
|
|
\cite{TEP05} the Featherweight Java-Calculus \textsf{Wild~ FJ} is introduced. It
|
|
contains a formal description of wildcards. The Java Language Specification
|
|
\cite{GoJoStBrBuSm23} refers to \textsf{Wild~FJ} for the introduction of
|
|
wildcards. In \cite{aModelForJavaWithWildcards} a formal model based of explicite existential types
|
|
is introduced and proven as sound. Additionally, for a subset of Java a
|
|
translation to the formal model is given, such that this subset is proven as
|
|
sound. In \cite{WildcardsNeedWitnessProtection} another core calculus is
|
|
introduced, which is proven as
|
|
sound, too. In this paper it is shown that the unsoundness of Java which is
|
|
discovered in \cite{AT16} is avoidable, even in the absence of nullness-aware type
|
|
system. In \cite{TamingWildcards} finally a framework is presented which combines
|
|
use-site variance (wildcards as in Java) and definition-site variance (as in Scala). For
|
|
instance, it can be used to add use-site variance to Scala and extend the Java
|
|
type system to infer the definition-site variance.
|
|
|
|
Our calculus is mixture ...
|
|
|
|
\subsection{Type inference}
|
|
Some object-oriented languages like Scala, C\#, and Java perform
|
|
\emph{local} type inference \cite{PT98,OZZ01}. Local type
|
|
inference means that missing type annotations are recovered using only
|
|
information from adjacent nodes in the syntax tree without long distance
|
|
constraints. For instance, the type of a variable initialized with a
|
|
non-functional expression or the return type of a method can be
|
|
inferred. However, method argument types, in particular for recursive
|
|
methods, cannot be inferred by local type inference.
|
|
|
|
Milner's algorithm $\mathcal{W}$ \cite{DBLP:journals/jcss/Milner78} is
|
|
the gold standard for global type inference for languages with
|
|
parametric polymorphism, which is used by ML-style languages. The fundamental idea
|
|
of the algorithm is to enforce type equality by many-sorted type
|
|
unification \cite{Rob65,MM82}. This approach is effective and results
|
|
in so-called principal types because many-sorted unification is
|
|
unitary, which means that there is at most one most general result.
|
|
|
|
Pl\"umicke \cite{Plue07_3} presents a first attempt to adopt Milner's
|
|
approach to Java. However, the presence of subtyping means that type
|
|
unification is no longer unitary, but still finitary. Thus, there is
|
|
no longer a single most general type, but any type is an instance of a
|
|
finite set of maximal types (for more details see Section
|
|
\ref{sec:unification}). Further work by the same author
|
|
\cite{plue15_2,plue17_2},
|
|
refines this approach by moving to a constraint-based algorithm and by
|
|
considering lambda expressions and Scale-like function types.
|
|
|
|
Pluemicke has a different approach to introduce wildcards in \cite{Plue09_1}. He
|
|
allows wildcards as any subsitution for type variables and disclaim the
|
|
capture conversion. Instead he extended
|
|
the subtyping ordering such that for $\theta \sub \theta' \sub \theta''$ holds
|
|
indeed the transitiv closure of $\QMextends{\theta} \sub \theta'$ and $\theta' \sub
|
|
\QMsuper{\theta''}$ but not the reflexive closure. He gave a type unification
|
|
algorithm for this type system, which he proved as sound and complete.
|
|
|
|
The problem of his type system is in the lossing reflexivity as shown in
|
|
example \ref{intro-example1}. First approaches to solve this problem he gave in
|
|
\cite{plue24_1}, where he fixes that no pairwise different nodes in the
|
|
abstract syntax gets the same type variable and that no pairwise different type
|
|
variables are equalized. In \cite{PH23} he showed how his type inference
|
|
algorithm suffices theese properties.
|
|
|
|
In Pl\"umicke's work there is indeed a formal definition of the subtying
|
|
ordering and a correctness proof of the type unification algorithms but no
|
|
soundness proof of the type system, itself. Therefore we choose for our type
|
|
inference algorithms with wildcars the approach of ???????
|
|
|