From bbe5d4f065009acee360377c910a11ef7c87d10c Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Wed, 17 Apr 2024 00:11:16 +0200
Subject: [PATCH] Fix Input/Output syntax

---
 introduction.tex | 46 +++++++++++++++-------------------------------
 1 file changed, 15 insertions(+), 31 deletions(-)

diff --git a/introduction.tex b/introduction.tex
index 39f43ad..8a16888 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -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}