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

Add ANF transformation. Define LetFJ. Change Constraint generation. Cleanup old explanation of Capture conversion. Add example to Constraint generation

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-03-30 00:07:26 +01:00
parent 7b86dc0cf3
commit 87f413241a
4 changed files with 341 additions and 347 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

291
constraints.tex
View File

@ -9,19 +9,22 @@
%\subsection{Well-Formedness} %\subsection{Well-Formedness}
Constraint generation step is the same as in \cite{TIforFGJ} except for field access and method invocation.
Here \fjtype{} generates capture constraints instead of normal subtype constraints.
Subtype constraints are created according to the type rules defined in section \ref{sec:tifj}. % But it can be easily adapted to Featherweight Java or Java.
The \typeExpr{} function creates constraints for a given expression. % We add T <. a for every return of an expression anyway. If anything returns a Generic like X it is not directly used in a method call like X <c T
$\begin{array}{c} The constraint generation works on the \TamedFJ{} language.
\typeExpr(\texttt{t}_1, \ntv{b}) = C_l \quad \quad \typeExpr(\texttt{t}_2, \ntv{c}) = C_l \quad \quad \ntv{b}, \ntv{c} \ \text{fresh} This step is mostly same as in \cite{TIforFGJ} except for field access and method invocation.
\\ We will focus on those parts.
\hline Here the new capture constraints and wildcard type placeholders are introduced.
\typeExpr(\texttt{t}_1 \texttt{?:} \texttt{t}_2, \tv{a}) = C_l \cup C_r \cup \set{\ntv{b} \lessdot \tv{a}, \ntv{c} \lessdot \tv{a}}
\end{array} Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj}
$ Unknown types at the time of the constraint generation step are replaced with type placeholders.
\begin{verbatim}
m(l, v){
let x = x in x.add(v)
}
\end{verbatim}
The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call. The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion. Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
@ -68,7 +71,7 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
\begin{align*} \begin{align*}
% Type % Type
\type{T}, \type{U} &::= \tv{a} \mid \wtv{a} \mid \mv{X} \mid {\wcNtype{\Delta}{N}} && \text{types and type placeholders}\\ \type{T}, \type{U} &::= \tv{a} \mid \wtv{a} \mid \mv{X} \mid {\wcNtype{\Delta}{N}} && \text{types and type placeholders}\\
\type{N} &::= \exptype{C}{\il{T}} && \text{class type (with type variables)} \\ \type{N} &::= \exptype{C}{\ol{T}} && \text{class type (with type variables)} \\
% Constraints % Constraints
\constraint &::= \type{T} \lessdot \type{U} \mid \type{T} \lessdotCC \type{U} && \text{Constraint}\\ \constraint &::= \type{T} \lessdot \type{U} \mid \type{T} \lessdotCC \type{U} && \text{Constraint}\\
\consSet &::= \set{\constraints} && \text{constraint set}\\ \consSet &::= \set{\constraints} && \text{constraint set}\\
@ -90,21 +93,17 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
\begin{figure}[tp] \begin{figure}[tp]
\begin{gather*} \begin{gather*}
\begin{array}{@{}l@{}l} \begin{array}{@{}l@{}l}
\fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, K \, \overline{M} \}}) =\\ \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
& \begin{array}{ll@{}l} & \begin{array}{ll@{}l}
\textbf{let} & \forall \texttt{m} \in \ol{M}: \tv{a}_\texttt{m}, \ol{\tv{a}_m} \ \text{fresh} \\ \textbf{let} & \ol{\methodAssumption} =
& \ol{\methodAssumption} = \begin{array}[t]{l} \set{ \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \mid
\set{ \mv{m'} : (\exptype{C}{\ol{X} \triangleleft \ol{N}} \to \ol{\tv{a}} \to \tv{a}) \mid \set{ \mv{m}(\ol{x}) = \expr{e} } \in \ol{M}, \, \tv{a}, \ol{\tv{a}}\ \text{fresh} } \\
\mv{m'} \in \ol{M} \setminus \set{\mv{m}}, \, \tv{a}\, \ol{\tv{a}}\ \text{fresh} } \\ \textbf{in}
\ \cup \, \set{\mv{m} : (\exptype{C}{\ol{X} \triangleleft \ol{N}} \to \ol{\tv{a}_m} \to \tv{a}_\mv{m})} & \begin{array}[t]{l}
\end{array} \set{ \typeExpr(\mtypeEnvironment \cup \ol{\methodAssumption} \cup \set{\mv{this} :
\\ \exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}} }, \texttt{e}, \tv{a})
& C_m = \typeExpr(\mtypeEnvironment \cup \set{\mv{this} : \\ \quad \quad \quad \quad \mid \set{ \mv{m}(\ol{x}) = \expr{e} } \in \ol{M},\, \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \in \ol{\methodAssumption}}
\exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}_m} }, \texttt{e}, \tv{a}_\texttt{m}) \\ \end{array}
\textbf{in}
& { ( \mtypeEnvironment \cup \ol{\methodAssumption}, \,
\bigcup_{\texttt{m} \in \ol{M}} C_m )
}
\end{array} \end{array}
\end{array} \end{array}
\end{gather*} \end{gather*}
@ -112,56 +111,6 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
\label{fig:constraints-for-classes} \label{fig:constraints-for-classes}
\end{figure} \end{figure}
% \textbf{Method Assumptions}
% %$\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm.
% % \begin{verbatim}
% % class Example<X> {
% % <Y> Y m(Example<Y> p){ ... }
% % }
% % \end{verbatim}
% In Featherweight Java a method type is bound to a specific class.
% The class \texttt{Example} shown above contains one method \texttt{m}:
% \begin{displaymath}
% \textit{mtype}({\texttt{m}, \exptype{Example}{\type{X}}}) = \generics{\type{Y}} \ \exptype{Example}{\type{Y}} \to \type{Y}
% \end{displaymath}
% $\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm.
% It's a map of method types to method names.
% Every method name has a set of possible types,
% because there could be more than one method with the same name in a program consisting out of multiple classes.
% To simplify the syntax of method assumptions, we add the inheriting class type to the parameter list:
% \begin{displaymath}
% \Pi = \set{ \texttt{m} : \generics{\type{X}, \type{Y}} \ (\exptype{Example}{\type{X}}, \exptype{Example}{\type{Y}}) \to \type{Y}}
% \end{displaymath}
% \begin{verbatim}
% class Example<X> { }
% <X, Y> Y m(Example<X> this, Example<Y> p){ ... }
% \end{verbatim}
\begin{displaymath}
\begin{array}{@{}l@{}l}
\typeExpr{} &({\mtypeEnvironment} , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2) = \\
& \begin{array}{ll}
\textbf{let}
& \tv{e}, \tv{x} \ \text{fresh} \\
& \consSet_R = \typeExpr({\mtypeEnvironment}, \expr{e}_1, \tv{e})\\
& \constraint =
\set{
\tv{e} \lessdot \tv{x}
}\\
{\mathbf{in}} & {
\consSet_R \cup \set{\constraint}} \cup \typeExpr(\mtypeEnvironment \cup \set{\expr{x} : \tv{x}})
\end{array}
\end{array}
\end{displaymath}
\begin{displaymath} \begin{displaymath}
\begin{array}{@{}l@{}l} \begin{array}{@{}l@{}l}
\typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\ \typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\
@ -185,13 +134,27 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
\end{array} \end{array}
\end{displaymath} \end{displaymath}
The set of method assumptions returned by the \textit{mtypes} function is used to generate the constraints for a method call expression:
There are two kinds of method calls.
The ones to already typed methods and calls to untyped methods.
\begin{displaymath} \begin{displaymath}
\begin{array}{@{}l@{}l} \begin{array}{@{}l@{}l}
\typeExpr{}' & ({\mtypeEnvironment} , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\ \typeExpr{} &({\mtypeEnvironment} , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2, \tv{a}) = \\
& \begin{array}{ll}
\textbf{let}
& \tv{e}_1, \tv{e}_2, \tv{x} \ \text{fresh} \\
& \consSet_1 = \typeExpr({\mtypeEnvironment}, \expr{e}_1, \tv{e}_1)\\
& \consSet_2 = \typeExpr({\mtypeEnvironment} \cup \set{\expr{x} : \tv{x}}, \expr{e}_2, \tv{e}_2)\\
& \constraint =
\set{
\tv{e}_1 \lessdot \tv{x}, \tv{e}_2 \lessdot \tv{a}
}\\
{\mathbf{in}} & {
\consSet_1 \cup \consSet_2 \cup \set{\constraint}}
\end{array}
\end{array}
\end{displaymath}
\begin{displaymath}
\begin{array}{@{}l@{}l}
\typeExpr{} & ({\mtypeEnvironment} , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
& \begin{array}{ll} & \begin{array}{ll}
\textbf{let} \textbf{let}
& \tv{r}, \ol{\tv{r}} \text{ fresh} \\ & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
@ -207,126 +170,98 @@ The ones to already typed methods and calls to untyped methods.
\end{array} \end{array}
\end{array} \end{array}
\end{displaymath} \end{displaymath}
\begin{displaymath}
\begin{array}{@{}l@{}l}
\typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a}) = \\
& \begin{array}{ll}
\textbf{let}
& \tv{r}, \ol{\tv{r}} \text{ fresh} \\
& \consSet_R = \typeExpr(({\mtypeEnvironment} ;
\overline{\localVarAssumption}), \texttt{e}, \tv{r})\\
& \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \ol{e}, \ol{\tv{r}}) \\
& \begin{array}{@{}l@{}l}
\constraint = \orCons\set{ &
\begin{array}[t]{l}
[\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}},
\overline{\tv{r}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a},
\ol{Y} \lessdot \ol{N} \}
\end{array}\\
& \ |\
(\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T}) \in
{\mtypeEnvironment} %, \, |\ol{T}| = |\ol{e}|
, \, \overline{\wtv{a}} \text{ fresh}}
\end{array}\\
\mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T})
\end{array}
\end{array}
\end{displaymath}
\\[1em] \\[1em]
\noindent \noindent
\textbf{Example:} \textbf{Example:}
\begin{verbatim} \begin{verbatim}
class Class1{ class Class1{
<X> X m(List<X> lx, List<? extends X> lt){ ... } <A> A head(List<X> l){ ... }
List<? extends String> wGet(){ ... } List<? extends String> get() { ... }
List<String> get() { ... }
} }
class Class2{ class Class2{
example(c1){ example(c1){
return c1.m(c1.get(), c1.wGet()); return c1.head(c1.get());
} }
} }
\end{verbatim} \end{verbatim}
%This example comes with predefined type annotations. %This example comes with predefined type annotations.
We assume the class \texttt{Class1} has already been processed by our type inference algorithm, We assume the class \texttt{Class1} has already been processed by our type inference algorithm
which has lead to the given type annotations for \texttt{Class1}. leading to the following type annotations:
Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class: %Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class:
\begin{displaymath} \begin{displaymath}
\mtypeEnvironment = \left\{\begin{array}{l} \mtypeEnvironment = \left\{\begin{array}{l}
\type{Class1}.\texttt{m}: \generics{\type{X} \triangleleft \type{Object}} \ \texttt{m}: \generics{\type{A} \triangleleft \type{Object}} \
(\exptype{List}{\type{X}}, \, \wctype{\wildcard{A}{\type{X}}{\bot}}{List}{\wildcard{A}{\type{X}}{\bot}}) \to \type{X}, \\ (\type{Class1},\, \exptype{List}{\type{A}}) \to \type{X}, \\
\type{Class1}.\texttt{wGet}: () \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\wildcard{A}{\type{Object}}{\type{String}}}, \\ \texttt{get}: (\type{Class1}) \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\rwildcard{A}}
\type{Class1}.\texttt{get}: () \to \exptype{List}{\type{String}}
\end{array} \right\} \end{array} \right\}
\end{displaymath} \end{displaymath}
The result of the $\typeExpr{}$ function is the constraint set At first we have to convert the example method to a syntactically correct \TamedFJ{} program.
\begin{displaymath} Afterwards the the \fjtype{} algorithm is able to generate constraints.
C = \left\{ \begin{array}{l}
\tv{c1} \lessdot \type{Class1}, \\
\tv{p1} \lessdot \exptype{List}{\wtv{x}}, \\
\exptype{List}{\type{String}} \lessdot \tv{p1}, \\
\tv{p2} \lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}}, \\
\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{p2}
\end{array} \right\}
\end{displaymath}
\begin{minipage}{0.45\textwidth}
\begin{lstlisting}[style=tamedfj]
class Class2 {
example(c1) = let x = c1 in
let xp = x.get() in x.m(xp);
}
\end{lstlisting}
\end{minipage}%
\hfill
\begin{minipage}{0.5\textwidth}
\begin{constraintset}
$
\begin{array}{l}
\ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}, \\
\ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}, \\
\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{xp}, \\
\tv{xp} \lessdotCC \exptype{List}{\wtv{a}}
\end{array}
$
\end{constraintset}
\end{minipage}
The first parameter of a method assumption is the receiver type $\type{T}_r$. Following is a possible solution for the given constraint set:
\texttt{Class1} for this example.
Therefore the $(\tv{c1} \lessdot \type{Class1})$ constraint.
The type variable $\tv{c1}$ is assigned to the parameter \texttt{c1} of the \texttt{example} method.
or a simplified version: \begin{minipage}{0.55\textwidth}
\begin{lstlisting}[style=letfj]
class Class2 {
example(c1) = let x : Class1 = c1 in
let xp : (*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*) = x.get()
in x.m(xp);
}
\end{lstlisting}
\end{minipage}%
\hfill
\begin{minipage}{0.4\textwidth}
\begin{constraintset}
$
\begin{array}{l}
\sigma(\ntv{x}) = \type{Class1} \\
%\tv{xp} \lessdot \exptype{List}{\wtv{x}}, \\
%\exptype{List}{\type{String}} \lessdot \tv{p1}, \\
\sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \\
\end{array}
$
\end{constraintset}
\end{minipage}
\begin{displaymath} For $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$ to be a correct solution for $\tv{xp}$
C = \left\{ \begin{array}{l} the constraint $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{a}}$
\tv{c1} \lessdot \type{Class1}, \\ must be satisfied.
\exptype{List}{\type{String}} This is possible, because we deal with a capture constraint.
\lessdot \exptype{List}{\wtv{x}}, \\ The $\lessdotCC$ constraint allows the left side to undergo a capture conversion
\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} which leads to $\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{a}}$.
\lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}} Now a substitution of the wildcard placeholder $\wtv{a}$ with $\rwildcard{A}$ leads to a satisfied constraint set.
\end{array} \right\}
\end{displaymath}
The wildcard placeholders are not used as parameter or return types of methods.
$\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as a free type variable. Or as types for variables introduced by let statements.
%TODO: Do an example where wildcards are inserted and we need capture conversion They are only used for generic method parameters during a method invocation.
Type placeholders which are not flagged as wildcard placeholders ($\wtv{a}$) can never hold a free variable or a type containing free variables.
\unify{} returns the solution $(\sigma = \set{ \tv{x} \to \type{String} })$ This practice hinders free variables to leave their scope.
The free variable $\rwildcard{A}$ generated by the capture conversion on the type $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$
% \\[1em] cannot be used anywhere else then inside the constraints generated by the method call \texttt{x.m(xp)}.
% \noindent
% \textbf{Example:}
% \begin{verbatim}
% class Class1 {
% <X> Pair<X, X> make(List<X> l){ ... }
% <Y> boolean compare(Pair<Y,Y> p) { ... }
% example(l){
% return compare(make(l));
% }
% }
% \end{verbatim}
% The method call \texttt{make(l)} generates the constraints
% \begin{displaymath}
% \tv{l} \lessdot \exptype{List}{\tv{x}}, \exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m}
% \end{displaymath}
% with $\tv{l}$ being the type placeholder for the variable \texttt{l}
% and $\tv{m}$ is the type variable for the return type of the method call.
% $\tv{m}$ is then used as the parameter for the \texttt{compare} method:
% \begin{displaymath}
% \tv{m} \lessdot \exptype{Pair}{\tv{y}, \tv{y}}
% \end{displaymath}
% Note the conversion of the generic parameters \texttt{X} and \texttt{Y} to type variables $\tv{x}$ and $\tv{y}$.
% Step 3 of the \unify{} algorithm has to look for every possible supertype of $\exptype{Pair}{\tv{x}, \tv{x}}$,
% when processing the $\exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m}$ constraint.
\begin{displaymath} \begin{displaymath}
\begin{array}{@{}l@{}l} \begin{array}{@{}l@{}l}

322
introduction.tex
View File

@ -382,6 +382,91 @@ $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype
% List<?> m() = new List<String>() :? new List<Integer>() :? id(m()); % List<?> m() = new List<String>() :? new List<Integer>() :? id(m());
% \end{verbatim} % \end{verbatim}
\subsection{\TamedFJ{} and \letfj{}}
%LetFJ -> Output language!
%TamedFJ -> ANF transformed input langauge
%Input language only described here. It is standard Featherweight Java
% we use the transformation to proof soundness. this could also be moved to the end.
% the constraint generation step assumes every method argument to be encapsulated in a let statement. This is the way Java is doing capture conversion
The input to our algorithm is a typeless version of Featherweight Java.
Methods are declared without parameter or return types.
We still keep type annotations for fields and generic class parameters.
This is a design choice by us,
as we consider them as data declarations which are given by the programmer.
% They are inferred in for example \cite{plue14_3b}
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 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.
\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} & ::= & \generics{\overline{\type{X} \triangleleft \type{N}}}\type{T}\ \texttt{m}(\overline{\type{T}\ \expr{x}}) = \expr{e} \\
\text{Terms} & \expr{e} & ::= & \expr{x} \\
& & \ \ | & \texttt{new} \ \exptype{C}{\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} \elvis{} \expr{e}\\
\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
\hline
\end{array}
$
\caption{Output Syntax}\label{fig:outputSyntax}
\end{figure}
The output of our type inference algorithm is a valid \letfj{} program.
Before generating constraints the input is transformed to \TamedFJ{}.
After adding the missing type annotations the resulting program is a valid \letfj{} program.
%This is shown in chapter \ref{sec:soundness}
Capture conversion is only needed for wildcard types,
but we don't know which expressions will spawn wildcard types because there are no type annotations yet.
We preemptively enclose every expression in a let statement before using it as a method argument.
We need the let statements to deal with possible Wildcard types.
The syntax used in our examples is the standard Featherweight Java syntax.
\subsection{Challenges}\label{challenges} \subsection{Challenges}\label{challenges}
%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards} %TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
@ -414,7 +499,7 @@ it is safe to pass \texttt{"String"} for the first parameter of the function.
<A> List<A> add(List<A> l, A v) {} <A> List<A> add(List<A> l, A v) {}
List<? super String> list = ...; List<? super String> list = ...;
add("String", list); add(list, "String");
\end{verbatim} \end{verbatim}
\end{example} \end{example}
@ -460,7 +545,7 @@ class SpecialPair<X, Y extends X> extends Pair<X,Y>{}
<X,Y> Pair<X,Y> id(Pair<X,Y> in){ <X,Y> Pair<X,Y> id(Pair<X,Y> in){
return ...; return in;
} }
<X, Y extends X> void receive(Pair<X,Y> in){} <X, Y extends X> void receive(Pair<X,Y> in){}
@ -531,154 +616,121 @@ $
The \unify{} algorithm only sees the constraints with no information about the program they originated from. The \unify{} algorithm only sees the constraints with no information about the program they originated from.
The main challenge was to find an algorithm which computes $\sigma(\wtv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}. The main challenge was to find an algorithm which computes $\sigma(\wtv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}.
\section{\TamedFJ{} and \letfj{}}
The input to our type inference algorithm is a \TamedFJ{} program.
The output is a valid \letfj{} program.
\letfj{} is defined in \cite{WildcardsNeedWitnessProtection}.
It is an extension to Featherweight Java which adds Wildcard types and let statements.
The let statements are used to explicitly apply capture conversion.
%TODO %TODO
% The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards} % The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards}
% and \cite{WildcardsNeedWitnessProtection}. % and \cite{WildcardsNeedWitnessProtection}.
\subsection{Capture Conversion} % \subsection{Capture Conversion}
The input to our type inference algorithm does not contain let statements. % The \texttt{let} statements in \TamedFJ{} act as capture conversion for wildcard types.
Those are added after computing a type solution.
Let statements act as capture conversion and only have to be applied in method calls involving wildcard types.
\begin{figure} % \begin{figure}
\begin{minipage}{0.45\textwidth} % \begin{minipage}{0.45\textwidth}
\begin{lstlisting}[style=fgj] % \begin{lstlisting}[style=tfgj]
<X> List<X> clone(List<X> l); % <X> List<X> clone(List<X> l);
example(p){ % example(p){
return clone(p); % return clone(p);
} % }
\end{lstlisting} % \end{lstlisting}
\end{minipage}% % \end{minipage}%
\hfill % \hfill
\begin{minipage}{0.5\textwidth} % \begin{minipage}{0.5\textwidth}
\begin{lstlisting}[style=tfgj] % \begin{lstlisting}[style=letfj]
(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){ % <X> List<X> clone(List<X> l);
return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in % (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p) =
clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*); % let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in
} % clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
\end{lstlisting} % \end{lstlisting}
\end{minipage} % \end{minipage}
\caption{Type inference adding capture conversion}\label{fig:addingLetExample} % \caption{Type inference adding capture conversion}\label{fig:addingLetExample}
\end{figure} % \end{figure}
Figure \ref{fig:addingLetExample} shows a let statement getting added to the typed output. % Figure \ref{fig:addingLetExample} shows a let statement getting added to the typed output.
The method \texttt{clone} cannot be called with the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$. % The method \texttt{clone} cannot be called with the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
After a capture conversion \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ with $\rwildcard{X}$ being a free variable. % After a capture conversion \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ with $\rwildcard{X}$ being a free variable.
Afterwards we have to find a supertype of $\exptype{List}{\rwildcard{X}}$, which does not contain free variables % Afterwards we have to find a supertype of $\exptype{List}{\rwildcard{X}}$, which does not contain free variables
($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in this case). % ($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in this case).
During the constraint generation step most types are not known yet and are represented by a type placeholder. % During the constraint generation step most types are not known yet and are represented by a type placeholder.
During a methodcall like the one in the \texttt{example} method in figure \ref{fig:ccExample} the type of the parameter \texttt{p} % During a methodcall like the one in the \texttt{example} method in figure \ref{fig:ccExample} the type of the parameter \texttt{p}
is not known yet. % is not known yet.
The type \texttt{List<?>} would be one possibility as a parameter type for \texttt{p}. % The type \texttt{List<?>} would be one possibility as a parameter type for \texttt{p}.
To make wildcards work for our type inference algorithm \unify{} has to apply capture conversions if necessary. % To make wildcards work for our type inference algorithm \unify{} has to apply capture conversions if necessary.
The type placeholder $\tv{r}$ is the return type of the \texttt{example} method. % The type placeholder $\tv{r}$ is the return type of the \texttt{example} method.
One possible type solution is $\tv{p} \doteq \tv{r} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$, % One possible type solution is $\tv{p} \doteq \tv{r} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$,
which leads to: % which leads to:
\begin{verbatim} % \begin{verbatim}
List<?> example(List<?> p){ % List<?> example(List<?> p){
return clone(p); % return clone(p);
} % }
\end{verbatim} % \end{verbatim}
But by substituting $\tv{p} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in the constraint % But by substituting $\tv{p} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in the constraint
$\tv{p} \lessdotCC \exptype{List}{\wtv{x}}$ leads to % $\tv{p} \lessdotCC \exptype{List}{\wtv{x}}$ leads to
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$. % $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$.
To make this typing possible we have to introduce a capture conversion via a let statement: % To make this typing possible we have to introduce a capture conversion via a let statement:
$\texttt{return}\ (\texttt{let}\ \texttt{x} : \wctype{\rwildcard{X}}{List}{\rwildcard{X}} = \texttt{p}\ \texttt{in} \ % $\texttt{return}\ (\texttt{let}\ \texttt{x} : \wctype{\rwildcard{X}}{List}{\rwildcard{X}} = \texttt{p}\ \texttt{in} \
\texttt{clone}\generics{\rwildcard{X}}(x) : \wctype{\rwildcard{X}}{List}{\rwildcard{X}})$ % \texttt{clone}\generics{\rwildcard{X}}(x) : \wctype{\rwildcard{X}}{List}{\rwildcard{X}})$
Inside the let statement the variable \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ % Inside the let statement the variable \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$
This spawns additional problems. % This spawns additional problems.
\begin{figure} % \begin{figure}
\begin{minipage}{0.45\textwidth} % \begin{minipage}{0.45\textwidth}
\begin{verbatim} % \begin{verbatim}
<X> List<X> clone(List<X> l){...} % <X> List<X> clone(List<X> l){...}
example(p){ % example(p){
return clone(p); % return clone(p);
} % }
\end{verbatim} % \end{verbatim}
\end{minipage}% % \end{minipage}%
\hfill % \hfill
\begin{minipage}{0.35\textwidth} % \begin{minipage}{0.35\textwidth}
\begin{constraintset} % \begin{constraintset}
\textbf{Constraints:}\\ % \textbf{Constraints:}\\
$ % $
\tv{p} \lessdotCC \exptype{List}{\wtv{x}}, \\ % \tv{p} \lessdotCC \exptype{List}{\wtv{x}}, \\
\tv{p} \lessdot \tv{r}, \\ % \tv{p} \lessdot \tv{r}, \\
\tv{p} \lessdot \type{Object}, % \tv{p} \lessdot \type{Object},
\tv{r} \lessdot \type{Object} % \tv{r} \lessdot \type{Object}
$ % $
\end{constraintset} % \end{constraintset}
\end{minipage} % \end{minipage}
\caption{Type inference example}\label{fig:ccExample} % \caption{Type inference example}\label{fig:ccExample}
\end{figure} % \end{figure}
In addition with free variables this leads to unwanted behaviour. % In addition with free variables this leads to unwanted behaviour.
Take the constraint % Take the constraint
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ for example. % $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ for example.
After a capture conversion from $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ to $\exptype{List}{\rwildcard{Y}}$ and a substitution $\wtv{a} \doteq \rwildcard{Y}$ % After a capture conversion from $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ to $\exptype{List}{\rwildcard{Y}}$ and a substitution $\wtv{a} \doteq \rwildcard{Y}$
we get % we get
$\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$. % $\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$.
Which is correct if we apply capture conversion to the left side: % Which is correct if we apply capture conversion to the left side:
$\exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$ % $\exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
If the input constraints did not intend for this constraint to undergo a capture conversion then \unify{} would produce an invalid % If the input constraints did not intend for this constraint to undergo a capture conversion then \unify{} would produce an invalid
type solution due to: % type solution due to:
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \nless: \exptype{List}{\rwildcard{X}}$ % $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \nless: \exptype{List}{\rwildcard{X}}$
The reason for this is the \texttt{S-Exists} rule's premise % The reason for this is the \texttt{S-Exists} rule's premise
$\text{dom}(\Delta') \cap \text{fv}(\exptype{List}{\rwildcard{X}}) = \emptyset$. % $\text{dom}(\Delta') \cap \text{fv}(\exptype{List}{\rwildcard{X}}) = \emptyset$.
Additionally free variables are not allowed to leave the scope of a capture conversion % Capture constraints cannot be stored in a set.
introduced by a let statement. % $\wtv{a} \lessdotCC \wtv{b}$ is not the same as $\wtv{a} \lessdotCC \wtv{b}$.
%TODO we combat both of this with wildcard type placeholders (? flag) % Both constraints will end up the same after a substitution for both placeholders $\tv{a}$ and $\tv{b}$.
% But afterwards a capture conversion is applied, which can generate different types on the left sides.
Type placeholders which are not flagged as possible free variables ($\wtv{a}$) can never hold a free variable or a type containing free variables. % \begin{itemize}
Constraint generation places these standard place holders at method return types and parameter types. % \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Y}}$
\begin{lstlisting}[style=fgj] % \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Z}}$
<X> List<X> clone(List<X> l); % \end{itemize}
(*@$\red{\tv{r}}$@*) example((*@$\red{\tv{p}}$@*) p){ %
return clone(p); % Wildcards are not reflexive. A box of type $\wctype{\rwildcard{X}}{Box}{\rwildcard{X}}$
} % is able to hold a value of any type. It could be a $\exptype{Box}{String}$ or a $\exptype{Box}{Integer}$ etc.
\end{lstlisting} % Also two of those boxes do not necessarily contain the same type.
This prevents type solutions that contain free variables in parameter and return types. % But there are situations where it is possible to assume that.
When calling a method which already has a type annotation we have to consider adding a capture conversion in form of a let statement. % For example the type $\wctype{\rwildcard{X}}{Pair}{\exptype{Box}{\rwildcard{X}}, \exptype{Box}{\rwildcard{X}}}$
The constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ signals the \unify{} algorithm that here a capture conversion is possible. % is a pair of two boxes, which always contain the same type.
$\sigma(\tv{p}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, \sigma(\tv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, $ is a possible solution. % Inside the scope of the \texttt{Pair} type, the wildcard $\rwildcard{X}$ stays the same.
But only when adding a capture conversion:
\begin{lstlisting}[style=fgj]
<X> List<X> clone(List<X> l);
(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
}
\end{lstlisting}
Capture constraints cannot be stored in a set.
$\wtv{a} \lessdotCC \wtv{b}$ is not the same as $\wtv{a} \lessdotCC \wtv{b}$.
Both constraints will end up the same after a substitution for both placeholders $\tv{a}$ and $\tv{b}$.
But afterwards a capture conversion is applied, which can generate different types on the left sides.
\begin{itemize}
\item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Y}}$
\item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Z}}$
\end{itemize}
Wildcards are not reflexive. A box of type $\wctype{\rwildcard{X}}{Box}{\rwildcard{X}}$
is able to hold a value of any type. It could be a $\exptype{Box}{String}$ or a $\exptype{Box}{Integer}$ etc.
Also two of those boxes do not necessarily contain the same type.
But there are situations where it is possible to assume that.
For example the type $\wctype{\rwildcard{X}}{Pair}{\exptype{Box}{\rwildcard{X}}, \exptype{Box}{\rwildcard{X}}}$
is a pair of two boxes, which always contain the same type.
Inside the scope of the \texttt{Pair} type, the wildcard $\rwildcard{X}$ stays the same.

3
prolog.tex
View File

@ -13,7 +13,8 @@
} }
\lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}} \lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}}
\lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}} \lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}}
\lstdefinestyle{letfj}{backgroundcolor=\color{lightgray!20}} \lstdefinestyle{letfj}{backgroundcolor=\color{lime!20}}
\lstdefinestyle{tamedfj}{backgroundcolor=\color{yellow!20}}
\lstdefinestyle{java}{backgroundcolor=\color{lightgray!20}} \lstdefinestyle{java}{backgroundcolor=\color{lightgray!20}}
\newtheorem{recap}[note]{Recap} \newtheorem{recap}[note]{Recap}

72
tRules.tex
View File

@ -61,7 +61,7 @@ $
\hline \hline
\end{array} \end{array}
$ $
\caption{Input Syntax}\label{fig:syntax} \caption{\TamedFJ{} Syntax}\label{fig:syntax}
\end{figure} \end{figure}
% \begin{figure} % \begin{figure}
@ -139,15 +139,16 @@ Featherweight Java's syntax involves no \texttt{let} statement
and terms can be nested freely. and terms can be nested freely.
This is similar to Java's syntax. This is similar to Java's syntax.
To convert it to \TamedFJ{} additional let statements have to be added. To convert it to \TamedFJ{} additional let statements have to be added.
This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation. This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation shown in figure \ref{fig:anfTransformation}.
The input of this transformation is a Featherweight Java program in the syntax given \ref{fig:inputSyntax}
and the output is a \TamedFJ{} program.
\textit{Example:}\\ \textit{Example:}\\
\noindent \noindent
\begin{minipage}{0.45\textwidth} \begin{minipage}{0.45\textwidth}
\begin{lstlisting}[style=fgj,caption=Featherweight Java] \begin{lstlisting}[style=fgj,caption=Featherweight Java]
m(l, v){ m(l, v){
return id(l).add(v); return l.add(v);
} }
\end{lstlisting} \end{lstlisting}
\end{minipage}% \end{minipage}%
@ -155,42 +156,48 @@ m(l, v){
\begin{minipage}{0.5\textwidth} \begin{minipage}{0.5\textwidth}
\begin{lstlisting}[style=tfgj,caption=\TamedFJ{} representation] \begin{lstlisting}[style=tfgj,caption=\TamedFJ{} representation]
m(l, v) = m(l, v) =
let x = id(l) in x.add(v) let x1 = l in
let x2 = v in x1.add(x2)
\end{lstlisting} \end{lstlisting}
\end{minipage} \end{minipage}
$ % $
\begin{array}{|lrcl|l} % \begin{array}{|lrcl|l}
\hline % \hline
& & & \textbf{Featherweight Java Terms}\\ % & & & \textbf{Featherweight Java Terms}\\
\text{Terms} & t & ::= % \text{Terms} & t & ::=
& \expr{x} % & \expr{x}
\\ % \\
& & \ \ | % & & \ \ |
& \texttt{new} \ \type{C}(\overline{t}) % & \texttt{new} \ \type{C}(\overline{t})
\\ % \\
& & \ \ | % & & \ \ |
& t.f % & t.f
\\ % \\
& & \ \ | % & & \ \ |
& t.\texttt{m}(\overline{t}) % & t.\texttt{m}(\overline{t})
\\ % \\
& & \ \ | % & & \ \ |
& t \elvis{} t\\ % & t \elvis{} t\\
% % %
\hline % \hline
\end{array} % \end{array}
$ % $
\begin{figure}
\begin{center}
$\begin{array}{lrcl} $\begin{array}{lrcl}
\text{ANF} & \anf{\expr{x}} & = & \expr{x} \\ %\text{ANF}
& \anf{\expr{x}} & = & \expr{x} \\
& \anf{\texttt{new} \ \type{C}(\overline{t})} & = & \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}}) \\ & \anf{\texttt{new} \ \type{C}(\overline{t})} & = & \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}}) \\
& \anf{t.f} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \expr{x}.f \\ & \anf{t.f} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \expr{x}.f \\
& \anf{t.\texttt{m}(\overline{t})} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \expr{x}.\texttt{m}(\overline{\expr{x}}) \\ & \anf{t.\texttt{m}(\overline{t})} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
& \anf{t_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2} & \anf{t_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2}
\end{array}$ \end{array}$
\end{center}
\caption{ANF Transformation}\label{fig:anfTransformation}
\end{figure}
% $ % $
% \begin{array}{lrcl|l} % \begin{array}{lrcl|l}
@ -455,7 +462,7 @@ $\begin{array}{l}
$\begin{array}{l} $\begin{array}{l}
\typerule{T-Let}\\ \typerule{T-Let}\\
\begin{array}{@{}c} \begin{array}{@{}c}
\Delta | \Gamma \vdash \expr{e}_1 : \type{T}_1 \quad \quad \Delta | \Gamma \vdash \expr{t}_1 : \type{T}_1 \quad \quad
\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N} \Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
\\ \\
\Delta, \Delta' | \Gamma, \expr{x} : \wcNtype{}{N} \vdash \expr{t}_2 : \type{T}_2 \quad \quad \Delta, \Delta' | \Gamma, \expr{x} : \wcNtype{}{N} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
@ -465,7 +472,7 @@ $\begin{array}{l}
\\ \\
\hline \hline
\vspace*{-0.3cm}\\ \vspace*{-0.3cm}\\
\Delta | \Gamma \vdash \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2 : \type{T} \Delta | \Gamma \vdash \texttt{let}\ \expr{x} = \expr{t}_1 \ \texttt{in} \ \expr{t}_2 : \type{T}
\end{array} \end{array}
\end{array}$ \end{array}$
\\[1em] \\[1em]
@ -508,8 +515,7 @@ $\begin{array}{l}
$\begin{array}{l} $\begin{array}{l}
\typerule{T-Class}\\ \typerule{T-Class}\\
\begin{array}{@{}c} \begin{array}{@{}c}
\mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \texttt{m} : (\type{T'_m}, \ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \quad \quad \mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \texttt{m} : (\exptype{C}{\ol{X}}, \ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \\
\forall \texttt{m} \in \ol{M}: \Delta \vdash \exptype{C}{\ol{X}} <: \type{T'_m}\\
\mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \texttt{m} : \mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \texttt{m} :
\generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M} } \\ \generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M} } \\
\triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad \triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad