stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Fixes and TODO

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-05-14 16:35:30 +02:00
parent bdfacdf3dd
commit 9e0d9ddd18
1 changed files with 8 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
introduction.tex
View File

@ -26,7 +26,7 @@ or allowing to write typeless Java code which is then type inferred and thereby
To outline the contributions in this paper we will list the advantages and improvements to smiliar type inference algorithms: To outline the contributions in this paper we will list the advantages and improvements to smiliar type inference algorithms:
\begin{description} \begin{description}
\item[Global Type Inference for Featherweight Java] \cite{TIforFGJ} is a predecessor to our algorithm. \item[Global Type Inference for Featherweight Java] \cite{TIforFGJ} is a predecessor to our algorithm.
The algorithm presented in this paper is a improved version The algorithm presented in this paper is an improved version
with the biggest change being the added wildcard support. with the biggest change being the added wildcard support.
% Proven sound on type rules of Featherweight Java, which are also proven to produce sound programs % Proven sound on type rules of Featherweight Java, which are also proven to produce sound programs
% implication rules that follow the subtyping rules directly. Easy to understand soundness proof % implication rules that follow the subtyping rules directly. Easy to understand soundness proof
@ -46,7 +46,7 @@ We try to keep the branching at a minimal amount to improve runtime behavior.
Also the transformation steps of the \unify{} algorithm are directly related to the subtyping rules of our calculus. Also the transformation steps of the \unify{} algorithm are directly related to the subtyping rules of our calculus.
\item[Java Type Inference] \item[Java Type Inference]
Java already provides type inference in a restricted form % namely {Local Type Inference}. Standard Java provides type inference in a restricted form % namely {Local Type Inference}.
which only works for local environments where the surrounding context has knwon types. which only works for local environments where the surrounding context has knwon types.
But our global type inference algorithm is able to work on input programs which do not hold any type annotations at all. But our global type inference algorithm is able to work on input programs which do not hold any type annotations at all.
We will show the different capabilities with an example. We will show the different capabilities with an example.
@ -95,6 +95,12 @@ Here our type inference algorithm based on unification is needed.
\subsection{Conclusion} \subsection{Conclusion}
% Additions: TODO
% - Global Type Inference Algorithm, no type annotations are needed
% - Soundness Proof
% - Easy to implement
% - Capture Conversion support
% - Existential Types support
\begin{itemize} \begin{itemize}
\item \item
We introduce the language \tifj{} (chapter \ref{sec:tifj}). We introduce the language \tifj{} (chapter \ref{sec:tifj}).