From 75dc20366d659b6cf30e703548d951432de61c68 Mon Sep 17 00:00:00 2001 From: "pl@gohorb.ba-horb.de" Date: Fri, 12 Apr 2024 00:25:47 +0200 Subject: [PATCH] modified: TIforWildFJ.tex modified: martin.bib modified: prolog.tex new file: relatedwork.tex --- TIforWildFJ.tex | 1 + martin.bib | 52 +++++++++++++++++++++++++++++++++++++ prolog.tex | 3 +++ relatedwork.tex | 69 +++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 125 insertions(+) create mode 100644 relatedwork.tex diff --git a/TIforWildFJ.tex b/TIforWildFJ.tex index ba64832..39f9ff5 100644 --- a/TIforWildFJ.tex +++ b/TIforWildFJ.tex @@ -146,6 +146,7 @@ class Example{ \include{soundness} %\include{termination} +\include{relatedwork} \bibliography{martin} diff --git a/martin.bib b/martin.bib index eece866..b759f02 100644 --- a/martin.bib +++ b/martin.bib @@ -50,6 +50,8 @@ keywords = {subtyping, type inference, principal types} SERIES = {Lecture Notes in Artificial Intelligence} } + + @article{DM82, author={Luis Damas and Robin Milner}, title={Principal type-schemes for functional programs}, @@ -65,6 +67,21 @@ keywords = {subtyping, type inference, principal types} pages={23-41}, month=Jan, 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, author = {Martelli, Alberto and Montanari, Ugo}, @@ -336,6 +353,14 @@ articleno = {138}, numpages = {22}, 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, author = {Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter}, title = {{Global Type Inference for Featherweight Generic Java}}, @@ -362,6 +387,16 @@ keywords = {Null, Java Wildcards, Existential Types} 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, title={Towards a semantic model for Java wildcards}, 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} } +@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)} +} + diff --git a/prolog.tex b/prolog.tex index 91422e5..6755733 100755 --- a/prolog.tex +++ b/prolog.tex @@ -71,6 +71,9 @@ \newcommand\subeq{\mathbin{\texttt{<:}}} \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{\generalizeRule}{General} diff --git a/relatedwork.tex b/relatedwork.tex new file mode 100644 index 0000000..62bf592 --- /dev/null +++ b/relatedwork.tex @@ -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 ??????? +