modified: TIforWildFJ.tex
modified: martin.bib modified: prolog.tex new file: relatedwork.tex
This commit is contained in:
parent
f5ddc65497
commit
75dc20366d
@ -146,6 +146,7 @@ class Example{
|
|||||||
|
|
||||||
\include{soundness}
|
\include{soundness}
|
||||||
%\include{termination}
|
%\include{termination}
|
||||||
|
\include{relatedwork}
|
||||||
|
|
||||||
\bibliography{martin}
|
\bibliography{martin}
|
||||||
|
|
||||||
|
52
martin.bib
52
martin.bib
@ -50,6 +50,8 @@ keywords = {subtyping, type inference, principal types}
|
|||||||
SERIES = {Lecture Notes in Artificial Intelligence}
|
SERIES = {Lecture Notes in Artificial Intelligence}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
@article{DM82,
|
@article{DM82,
|
||||||
author={Luis Damas and Robin Milner},
|
author={Luis Damas and Robin Milner},
|
||||||
title={Principal type-schemes for functional programs},
|
title={Principal type-schemes for functional programs},
|
||||||
@ -65,6 +67,21 @@ keywords = {subtyping, type inference, principal types}
|
|||||||
pages={23-41},
|
pages={23-41},
|
||||||
month=Jan,
|
month=Jan,
|
||||||
year={1965}}
|
year={1965}}
|
||||||
|
|
||||||
|
@article{DBLP:journals/jcss/Milner78,
|
||||||
|
author = {Robin Milner},
|
||||||
|
title = {A Theory of Type Polymorphism in Programming},
|
||||||
|
journal = {Journal of Computer and Systems Sciences},
|
||||||
|
volume = {17},
|
||||||
|
number = {3},
|
||||||
|
pages = {348--375},
|
||||||
|
year = {1978},
|
||||||
|
url = {https://doi.org/10.1016/0022-0000(78)90014-4},
|
||||||
|
doi = {10.1016/0022-0000(78)90014-4},
|
||||||
|
timestamp = {Tue, 16 Feb 2021 14:04:22 +0100},
|
||||||
|
biburl = {https://dblp.org/rec/journals/jcss/Milner78.bib},
|
||||||
|
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||||
|
}
|
||||||
|
|
||||||
@article{MM82,
|
@article{MM82,
|
||||||
author = {Martelli, Alberto and Montanari, Ugo},
|
author = {Martelli, Alberto and Montanari, Ugo},
|
||||||
@ -336,6 +353,14 @@ articleno = {138},
|
|||||||
numpages = {22},
|
numpages = {22},
|
||||||
keywords = {Null, Java Wildcards, Existential Types}
|
keywords = {Null, Java Wildcards, Existential Types}
|
||||||
}
|
}
|
||||||
|
@inproceedings{AT16,
|
||||||
|
author = {Amin, Nada and Tate, Ross},
|
||||||
|
year = {2016},
|
||||||
|
month = {10},
|
||||||
|
pages = {838-848},
|
||||||
|
title = {Java and scala's type systems are unsound: the existential crisis of null pointers},
|
||||||
|
doi = {10.1145/2983990.2984004}
|
||||||
|
}
|
||||||
@InProceedings{TIforFGJ,
|
@InProceedings{TIforFGJ,
|
||||||
author = {Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter},
|
author = {Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter},
|
||||||
title = {{Global Type Inference for Featherweight Generic Java}},
|
title = {{Global Type Inference for Featherweight Generic Java}},
|
||||||
@ -362,6 +387,16 @@ keywords = {Null, Java Wildcards, Existential Types}
|
|||||||
publisher={Addison-Wesley Professional}
|
publisher={Addison-Wesley Professional}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@Book{GoJoStBrBuSm23,
|
||||||
|
author = {Gosling, James and Joy, Bill and Steele, Guy and Bracha, Gilad and Buckley, Alex and Smith, Daniel},
|
||||||
|
title = "{The Java\textsuperscript{\textregistered} {L}anguage {S}pecification}",
|
||||||
|
Optpublisher = "Addison-Wesley",
|
||||||
|
url = {https://docs.oracle.com/javase/specs/jls/se21/jls21.pdf},
|
||||||
|
edition = {{J}ava {S}{E} 21},
|
||||||
|
year = 2023,
|
||||||
|
OPtseries = {The Java series}
|
||||||
|
}
|
||||||
|
|
||||||
@inproceedings{semanticWildcardModel,
|
@inproceedings{semanticWildcardModel,
|
||||||
title={Towards a semantic model for Java wildcards},
|
title={Towards a semantic model for Java wildcards},
|
||||||
author={Summers, Alexander J and Cameron, Nicholas and Dezani-Ciancaglini, Mariangiola and Drossopoulou, Sophia},
|
author={Summers, Alexander J and Cameron, Nicholas and Dezani-Ciancaglini, Mariangiola and Drossopoulou, Sophia},
|
||||||
@ -476,3 +511,20 @@ keywords = {Compilation, Java, generic classes, language design, language semant
|
|||||||
publisher={ACM New York, NY, USA}
|
publisher={ACM New York, NY, USA}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@InProceedings{PH23,
|
||||||
|
author = {Martin Pl{\"u}micke and Daniel Holle},
|
||||||
|
title = {Principal generics in {J}ava--{T}{X}},
|
||||||
|
booktitle = {Programmiersprachen und Grundlagen der Programmierung, 22. Kolloquium, KPS'23},
|
||||||
|
Optcrossref = {kps2023},
|
||||||
|
pages = {122--143},
|
||||||
|
year = {2023},
|
||||||
|
editor = {Thomas Noll and Ira Fesefeldt},
|
||||||
|
address = {Aachen},
|
||||||
|
number = {AIB-2023-03},
|
||||||
|
month = {September},
|
||||||
|
series = {Aachener Informatik-Berichte (AIB)},
|
||||||
|
url = {https://publications.rwth-aachen.de/record/972197/files/972197.pdf#%5B%7B%22num%22%3A281%2C%22gen%22%3A0%7D%2C%7B%22name%22%3A%22XYZ%22%7D%2C89.292%2C740.862%2Cnull%5D},
|
||||||
|
doi = {10.18154/RWTH-2023-10034},
|
||||||
|
Optnote = {(to appear)}
|
||||||
|
}
|
||||||
|
|
||||||
|
@ -71,6 +71,9 @@
|
|||||||
\newcommand\subeq{\mathbin{\texttt{<:}}}
|
\newcommand\subeq{\mathbin{\texttt{<:}}}
|
||||||
\newcommand\extends{\ensuremath{\triangleleft}}
|
\newcommand\extends{\ensuremath{\triangleleft}}
|
||||||
|
|
||||||
|
\newcommand{\QMextends}[1]{\textrm{\normalshape\ttfamily ?\,extends}\linebreak[0]\,#1}
|
||||||
|
\newcommand{\QMsuper}[1]{\textrm{\normalshape\ttfamily ?\linebreak[0]\,su\-per}\linebreak[0]\,#1}
|
||||||
|
|
||||||
\newcommand\rulename[1]{\textup{\textsc{(#1)}}}
|
\newcommand\rulename[1]{\textup{\textsc{(#1)}}}
|
||||||
\newcommand{\generalizeRule}{General}
|
\newcommand{\generalizeRule}{General}
|
||||||
|
|
||||||
|
69
relatedwork.tex
Normal file
69
relatedwork.tex
Normal file
@ -0,0 +1,69 @@
|
|||||||
|
|
||||||
|
\section{Related Work}
|
||||||
|
\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 ???????
|
||||||
|
|
Loading…
x
Reference in New Issue
Block a user