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

Fix Input/Output syntax

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-04-17 00:11:16 +02:00
parent 91f42d26f6
commit bbe5d4f065
1 changed files with 15 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
introduction.tex
View File

@ -59,6 +59,11 @@ emptyList().add(emptyList()).head().head()
In this example the return type of \texttt{emptyList} needs to consider that it should contain a list of a list.
This is a limitation of local type inference as presented here \cite{javaTIisBroken}.
% \begin{recap}{Java Local Type Inference}
% Local type inference is able to solve constraints of the form
% T <. b, b <. T where T are given types
% \end{recap}
% Local Type inference cannot infer F-Bounded types (TODO: we can, right?)
The big difference to local type inference is the ability to have constraints where both sides contain type placeholders.
As described in \cite{javaTIisBroken} local type inference is able to determine an unifier $\sigma$
which satisfies $\set{\overline{A <: \sigma(F)}, \sigma(R) <: E }$.
@ -465,37 +470,16 @@ Note the \texttt{new} expression not requiring generic parameters,
which are also inferred by our algorithm.
The method call naturally has no generic parameters aswell.
We add the elvis operator ($\elvis{}$) to the syntax mainly to showcase applications involving wildcard types.
The syntax is described in figure \ref{fig:inputSyntax}.
\begin{figure}
$
\begin{array}{lrcl}
\hline
\text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
\text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
\text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
\text{Type variable contexts} & \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
\text{Class declarations} & D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
\text{Method declarations} & \texttt{M} & ::= & \texttt{m}(\overline{x}) \{ \texttt{return}\ t; \} \\
\text{Terms} & t & ::= & x \\
& & \ \ | & \texttt{new} \ \type{C}(\overline{t})\\
& & \ \ | & t.f\\
& & \ \ | & t.\texttt{m}(\overline{t})\\
& & \ \ | & t \elvis{} t\\
\text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\
\hline
\end{array}
$
\caption{Input Syntax}\label{fig:inputSyntax}
\end{figure}
The syntax is described in figure \ref{fig:outputSyntax} with optional type annotations highlighted in yellow.
It is possible to exclude all optional types.
The output is a valid Featherweight Java program.
We use the syntax of the version introduced in \cite{WildcardsNeedWitnessProtection}
calling it \letfj{} for that it is a Featherweight Java variant including \texttt{let} statements.
Our output syntax is shown in figure \ref{fig:outputSyntax}
which is actually a subset of \letfj{}, because we omit \texttt{null} types.
% Our output syntax is shown in figure \ref{fig:outputSyntax}
% which is actually a subset of \letfj{}, because we omit \texttt{null} types.
\newcommand{\highlight}[1]{\begingroup\fboxsep=0pt\colorbox{yellow}{$\displaystyle #1$}\endgroup}
\begin{figure}
$
\begin{array}{lrcl}
@ -505,18 +489,18 @@ $
\text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
\text{Type variable contexts} & \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
\text{Class declarations} & D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
\text{Method declarations} & \texttt{M} & ::= & \generics{\overline{\type{X} \triangleleft \type{N}}}\type{T}\ \texttt{m}(\overline{\type{T}\ \expr{x}}) = \expr{e} \\
\text{Method declarations} & \texttt{M} & ::= & \highlight{\generics{\overline{\type{X} \triangleleft \type{N}}}}\ \highlight{\type{T}}\ \texttt{m}(\overline{\highlight{\type{T}}\ \expr{x}}) = \expr{e} \\
\text{Terms} & \expr{e} & ::= & \expr{x} \\
& & \ \ | & \texttt{new} \ \exptype{C}{\ol{T}}(\overline{\expr{e}})\\
& & \ \ | & \texttt{new} \ \type{C}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
& & \ \ | & \expr{e}.f\\
& & \ \ | & \expr{e}.\texttt{m}\generics{\ol{T}}(\overline{\expr{e}})\\
& & \ \ | & \texttt{let}\ \expr{x} : \wcNtype{\Delta}{N} = \expr{e} \ \texttt{in} \ \expr{e}\\
& & \ \ | & \expr{e}.\texttt{m}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
& & \ \ | & \texttt{let}\ \expr{x} \highlight{: \wcNtype{\Delta}{N}} = \expr{e} \ \texttt{in} \ \expr{e}\\
& & \ \ | & \expr{e} \elvis{} \expr{e}\\
\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
\hline
\end{array}
$
\caption{Output Syntax}\label{fig:outputSyntax}
\caption{Input Syntax with optional type annotations}\label{fig:outputSyntax}
\end{figure}