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

Restructure

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-05-23 14:18:50 +02:00
parent 2f5aa753e0
commit b2ca8e49df
3 changed files with 10 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
conclusion.tex
View File

@ -1,4 +1,10 @@
\section{Properties of the Algorithm}
\begin{itemize}
\item Our algorithm is designed for extensibility with the final goal of full support for Java.
\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
\end{itemize}
%TODO: how are the challenges solved: Describe this in the last chapter with examples!
\section{Soundness}\label{sec:soundness}

5
constraints.tex
View File

@ -184,7 +184,10 @@ A normal type placeholder cannot hold types containing free variables.
Normal type placeholders are assigned types which are also expressible with Java syntax.
So no types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ or $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
Type variables declared in the class header are passed to \unify{}.
It is possible to feed the \unify{} algorithm a set of free variables with predefined bounds.
This is used for class generics see figure \ref{fig:constraints-for-classes}.
The \fjtype{} function returns a set of constraints aswell as an initial environment $\Delta$
containing the generics declared by this class.
Those type variables count as regular types and can be held by normal type placeholders.
%Why do we need a constraint generation step?

3
tRules.tex
View File

@ -30,9 +30,6 @@ which by default is also a correct Featherweight Java program (see chapter \ref{
\begin{itemize}
\item The calculus does not include method overriding for simplicity reasons.
Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
Our algorithm is designed for extensibility with the final goal of full support for Java.
\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
%\textit{Note:}
\item The typing rules for expressions shown in figure \ref{fig:expressionTyping} refrain from restricting polymorphic recursion.
Type inference for polymorphic recursion is undecidable \cite{wells1999typability} and when proving completeness like in \cite{TIforFGJ} the calculus