From 77f3fbedfa83ee7824ea10dda3198f874f635ed5 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Mon, 13 May 2024 23:58:42 +0200 Subject: [PATCH] Cleanup and Restructure. Remove polymorphic recursion exclusion from Type Rules --- conclusion.tex | 114 ++++++++++++ constraints.tex | 101 +++++++++-- introduction.tex | 440 ++++++----------------------------------------- martin.bib | 11 ++ tRules.tex | 284 +++++++----------------------- unify.tex | 50 ++++-- 6 files changed, 369 insertions(+), 631 deletions(-) diff --git a/conclusion.tex b/conclusion.tex index 988cd4d..7fbd2de 100644 --- a/conclusion.tex +++ b/conclusion.tex @@ -1,3 +1,117 @@ +\section{Properties of the Algorithm} +\section{Soundness}\label{sec:soundness} + +\section{Completeness}\label{sec:completeness} +The algorithm can find a solution to every program which the Unify by Plümicke finds +a correct solution aswell. +It will not infer intermediat type like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X},\rwildcard{X}}$. +There is propably some loss of completeness when capture constraints get deleted. +This happens because constraints of the form $\tv{a} \lessdotCC \exptype{C}{\wtv{x}}$ are kept as long as possible. +Here the variable $\tv{a}$ maybe could hold a wildcard type, +but it gets resolved to a $\generics{\type{A} \triangleleft \type{N}}$. +This combined with a constraint $\type{N} \lessdot \wtv{x}$ looses a possible solution. + +This is our result: +\begin{verbatim} +class List { + void addTo(List l){ + l.add(this.get()); + } +} +\end{verbatim} +$ +\tv{l} \lessdotCC \exptype{List}{\wtv{y}}, +\type{X} \lessdot \wtv{y} +$ +But the most general type would be: +\begin{verbatim} +class List { + void addTo(List l){ + l.add(this.get()); + } +} +\end{verbatim} + +\subsection{Discussion Pair Example} +\begin{verbatim} + Pair make(List l){ ... } + boolean compare(Pair p) { ... } + +List l; +Pair p; + +compare(make(l)); // Valid +compare(p); // Error +\end{verbatim} + +Our type inference algorithm is not able to solve this example. +When we convert this to \TamedFJ{} and generate constraints we end up with: +\begin{lstlisting}[style=tamedfj] +let m = let x = l in make(x) in compare(m) +\end{lstlisting} +\begin{constraintset}$ +\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \ntv{x}, +\ntv{x} \lessdotCC \exptype{List}{\wtv{a}} +\exptype{Pair}{\wtv{a}, \wtv{a}} \lessdot \ntv{m}, %% TODO: Mark this constraint +\ntv{m} \lessdotCC \exptype{Pair}{\wtv{b}, \wtv{b}} +$\end{constraintset} + +$\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and +from the constraint +$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ +\unify{} deducts $\wtv{a} \doteq \rwildcard{X}$ leading to +$\exptype{Pair}{\rwildcard{X}, \rwildcard{X}} \lessdot \ntv{m}$. + +Finding a supertype to $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ is the crucial part. +The correct substition for $\ntv{m}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$. +But this leads to additional branching inside the \unify{} algorithm and increases runtime. +%We refrain from using that type, because it is not denotable with Java syntax. +%Types used for normal type placeholders should be expressable Java types. % They are not! + +The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax. + +\begin{lstlisting}[style=letfj] +let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l, m = make(x) in compare(make(x)) +\end{lstlisting} + +We can make it work with a special rule in the \unify{}. +But this will only help in this specific example and not generally solve the issue. +A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes: +$\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ and +$\wctype{\rwildcard{X}, \rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$. +Imagine a type $\exptype{Triple}{\rwildcard{X},\rwildcard{X},\rwildcard{X}}$ already has +% TODO: how many supertypes are there? +%X.Triple <: X,Y.Triple <: +%X,Y,Z.Triple + +% TODO example: +\begin{lstlisting}[style=java] + Triple sameL(List l) + Triple sameP(Pair l) + void triple(Triple tr){} + +Pair p ... +List l ... + +make(t) { return t; } +triple(make(sameP(p))); +triple(make(sameL(l))); +\end{lstlisting} + +\begin{constraintset} +$ +\exptype{Triple}{\rwildcard{X}, \rwildcard{X}, \rwildcard{X}} \lessdot \ntv{t}, +\ntv{t} \lessdotCC \exptype{Triple}{\wtv{a}, \wtv{b}, \wtv{b}}, \\ +(\textit{This constraint is added later: } \exptype{Triple}{\rwildcard{X}, \rwildcard{Y}, \rwildcard{Y}} \lessdot \ntv{t}) +$ +% Triple <. t +% ( Triple <. t ) <- this constraint is added later +% t <. Triple + +% t =. x.Triple +\end{constraintset} + + \section{Conclusion and Further Work} % we solved the problems given in the introduction (see examples TODO give names to examples) The problems introduced in the openening \ref{challenges} can be solved via our \unify{} algorithm (see examples \ref{example1} and \ref{example2}). diff --git a/constraints.tex b/constraints.tex index d3a282d..a921ee4 100644 --- a/constraints.tex +++ b/constraints.tex @@ -13,23 +13,104 @@ % But it can be easily adapted to Featherweight Java or Java. % 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 >} and proof this code snippet correct. The local type inference algorithm based on matching cannot produce this solution. Here our type inference algorithm based on unification is needed. -% \begin{verbatim} -% this.>emptyList().add(new List()) -% .get(0) -% .get(0); -% \end{verbatim} +\end{description} +% %motivate constraints: +% To solve this example our Type Inference algorithm will create constraints % $ -% \begin{array}[b]{c} -% \begin{array}[b]{c} -% \texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}} -% \\ -% \hline -% \texttt{emptyList().get()} : \exptype{List}{\type{String}} -% \end{array} \rulenameAfter{T-Call} -% \quad \generics{\type{X}}\exptype{List}{\type{X}} \to \type{X} \in \mtypeEnvironment{}(\texttt{get})1 -% \\ -% \hline -% \texttt{emptyList().get().get()} : \type{String} -% \end{array} \rulenameAfter{T-Call} +% \exptype{List}{\tv{a}} \lessdot \tv{b}, +% \tv{b} \lessdot \exptype{List}{\tv{c}}, +% \tv{c} \lessdot \exptype{List}{\tv{d}} % $ -%motivate constraints: -To solve this example our Type Inference algorithm will create constraints -$ -\exptype{List}{\tv{a}} \lessdot \tv{b}, -\tv{b} \lessdot \exptype{List}{\tv{c}}, -\tv{c} \lessdot \exptype{List}{\tv{d}} -$ - -% Local type inference cannot deal with type inference during the algorithm. -% If the left side contains unknown type parameters. -% \begin{verbatim} -% import java.util.ArrayList; -% import java.util.stream.*; - -% class Test { -% void test(){ -% var s = new ArrayList().stream().map(i -> 1); -% receive(s); -% } - -% void receive(Stream l){} -% } -% \end{verbatim} - -% TypeError: -% \begin{verbatim} -% void test(){ -% var l = new ArrayList(); -% l.add("hi"); -% var s = l.stream().map(i -> 1).collect(Collectors.toList()); -% var s2 = l.stream().map(i -> "String").collect(Collectors.toList()); -% receive(s, s2); -% } -% void receive(List l, List l2){} -% \end{verbatim} -% Correct: -% \begin{verbatim} -% void test(){ -% var l = new ArrayList(); -% l.add("hi"); -% List s = l.stream().map(i -> 1).collect(Collectors.toList()); -% List s2 = l.stream().map(i -> "String").collect(Collectors.toList()); -% receive(s, s2); -% } -% void receive(List l, List l2){} -% \end{verbatim} - -% Error: -% \begin{verbatim} -% rrr(this.emptyBox().set(this.emptyBox()).set(this.emptyBox())); -% \end{verbatim} -% Correct: -% \begin{verbatim} -% rrr(this.>emptyBox().set(this.emptyBox()).set(this.emptyBox())); -% \end{verbatim} - -% \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?) - -\section{Type Inference for Java} -%The goal is to find a correct typing for a given Java program. -Type inference for Java has many use cases and could be used to help programmers by inserting correct types for them, -finding better type solutions for already typed Java programs (for example more generical ones), -or allowing to write typeless Java code which is then type inferred and thereby type checked by our algorithm. -The algorithm proposed in this paper can determine a correct typing for the untyped Java source code example shown in figure \ref{fig:intro-example-typeless}. -Our algorithm is also capable of finding solutions involving wildcards as shown in listing \ref{lst:intro-example-typed}. - -%This paper extends a type inference algorithm for Featherweight Java \cite{TIforFGJ} by adding wildcards. -%The last step to create a type inference algorithm compatible to the Java type system. -The algorithm presented in this paper is a improved version of the one in \cite{TIforFGJ} including wildcard support. -% 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 -% capture conversion is needed -The type inference algorithm for Generic Featherweight Java \cite{TIforFGJ} produces \texttt{Object} as the return type of the -\texttt{genBox} method in listing \ref{lst:intro-example-typeless} -whereas our type inference algorithm will infer the type solution shown in listing \ref{lst:intro-example-typed}. -An existing unification algorithm for Java with wildcards \cite{plue09_1} states the same capabilities, -but exposes some when it comes to method invocations. -Especially the problems shown in chapter \ref{challenges} are handled incorrectly. -Whereas our type inference algorithm is based on a Featherweight Java calculus \cite{WildFJ} and it's proven sound subtyping rules. -%But they are all correctly solved by our new type inference algorithm presented in this paper. - +\subsection{Conclusion} \begin{itemize} \item We introduce the language \tifj{} (chapter \ref{sec:tifj}). @@ -201,7 +142,7 @@ genBox() { \end{minipage}% \hfill \begin{minipage}{0.55\textwidth} -\begin{lstlisting}[style=tfgj,caption=Correct type,label=lst:intro-example-typed] +\begin{lstlisting}[style=tfgj,caption=Type inference solution,label=lst:intro-example-typed] Box genBox() { if( ... ) { return new Box(1); @@ -221,7 +162,7 @@ Box genBox() { % \texttt{List} is not a valid return type for the method \texttt{genList}. % The type inference algorithm has to find the correct type involving wildcards (\texttt{List}). -\subsection{Java Wildcards} +\section{Java Wildcards} Java has invariant subtyping for polymorphic types. %but it incooperates use-site variance via so called wildcard types. @@ -271,7 +212,7 @@ but there exists some unknown type $\exptype{List}{\rwildcard{A}}$, with $\rwild Inside the body of the let statement \expr{v} is treated as a value with the constant type $\exptype{List}{\rwildcard{A}}$. Existential types enable us to formalize \textit{Capture Conversion}. Polymorphic method calls need to be wraped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}. -In Java this is done implicitly in a process called capture conversion. +In Java this is done implicitly in a process called capture conversion (as proposed in Wild FJ \cite{WildFJ}). \begin{figure} \begin{minipage}{0.4\textwidth} @@ -293,11 +234,6 @@ lo.add(new Integer(1)); // error! \end{minipage} \end{figure} -\begin{recap}{\textbf{Capture Conversion}} -TODO %Explain Java Capture Conversion - -\end{recap} - %show input and a correct letFJ representation %TODO: first show local type inference and explain lessdotCC constraints. then show example with global TI \begin{figure}[h] @@ -362,15 +298,17 @@ and \texttt{shuffle} can be invoked with the type parameter $\rwildcard{X}$: let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in shuffle(l2d') \end{lstlisting} -\subsection{Global Type Inference} +\section{Global Type Inference Algorithm} -\begin{description} - \item[input] \tifj{} program - \item[output] type solution - \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program -\end{description} +% \begin{description} +% \item[input] \tifj{} program +% \item[output] type solution +% \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program +% \end{description} -The input to our type inference algorithm is a modified version of the \letfj{}\cite{WildcardsNeedWitnessProtection} calculus (see chapter \ref{sec:tifj}). +%Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm. + +The input to our type inference algorithm is a modified version of the calculus in \cite{WildcardsNeedWitnessProtection} (see chapter \ref{sec:tifj}). First \fjtype{} generates constraints and afterwards \unify{} computes a solution for the given constraint set. Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$. @@ -501,71 +439,6 @@ $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype % List m() = new List() :? new List() :? id(m()); % \end{verbatim} -\subsection{\TamedFJ{}} -%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. -Method parameters and return types are optional. -We still require 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 type inferred 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: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. - -\newcommand{\highlight}[1]{\begingroup\fboxsep=0pt\colorbox{yellow}{$\displaystyle #1$}\endgroup} -\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} & ::= & \highlight{\generics{\overline{\type{X} \triangleleft \type{N}}}}\ \highlight{\type{T}}\ \texttt{m}(\overline{\highlight{\type{T}}\ \expr{x}}) \{ \texttt{return} \ \expr{e}; \} \\ -\text{Terms} & \expr{e} & ::= & \expr{x} \\ -& & \ \ | & \texttt{new} \ \type{C}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\ -& & \ \ | & \expr{e}.f\\ -& & \ \ | & \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{Input Syntax with optional type annotations}\label{fig:outputSyntax} -\end{figure} - -The output of our type inference algorithm is fully and correctly typed \TamedFJ{} program. - -Before generating constraints the input is transformed by an ANF transformation (see section \ref{sec:anfTransformation}). -Constraints are generated on the basis of the program in A-Normal form. -After adding the missing type annotations the resulting program is valid under the typing rules in \cite{WildFJ}. - -%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} %TODO: Wildcard subtyping is infinite see \cite{TamingWildcards} @@ -778,202 +651,3 @@ $\ntv{z}$ is a normal placeholder and is not allowed to contain free variables. %TODO: Move this part. or move the third challenge some underneath. 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}. - - -\section{Discussion Pair Example} -\begin{verbatim} - Pair make(List l){ ... } - boolean compare(Pair p) { ... } - -List l; -Pair p; - -compare(make(l)); // Valid -compare(p); // Error -\end{verbatim} - -Our type inference algorithm is not able to solve this example. -When we convert this to \TamedFJ{} and generate constraints we end up with: -\begin{lstlisting}[style=tamedfj] -let m = let x = l in make(x) in compare(m) -\end{lstlisting} -\begin{constraintset}$ -\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \ntv{x}, -\ntv{x} \lessdotCC \exptype{List}{\wtv{a}} -\exptype{Pair}{\wtv{a}, \wtv{a}} \lessdot \ntv{m}, %% TODO: Mark this constraint -\ntv{m} \lessdotCC \exptype{Pair}{\wtv{b}, \wtv{b}} -$\end{constraintset} - -$\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and -from the constraint -$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ -\unify{} deducts $\wtv{a} \doteq \rwildcard{X}$ leading to -$\exptype{Pair}{\rwildcard{X}, \rwildcard{X}} \lessdot \ntv{m}$. - -Finding a supertype to $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ is the crucial part. -The correct substition for $\ntv{m}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$. -But this leads to additional branching inside the \unify{} algorithm and increases runtime. -%We refrain from using that type, because it is not denotable with Java syntax. -%Types used for normal type placeholders should be expressable Java types. % They are not! - -The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax. - -\begin{lstlisting}[style=letfj] -let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l, m = make(x) in compare(make(x)) -\end{lstlisting} - -We can make it work with a special rule in the \unify{}. -But this will only help in this specific example and not generally solve the issue. -A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes: -$\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ and -$\wctype{\rwildcard{X}, \rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$. -Imagine a type $\exptype{Triple}{\rwildcard{X},\rwildcard{X},\rwildcard{X}}$ already has -% TODO: how many supertypes are there? -%X.Triple <: X,Y.Triple <: -%X,Y,Z.Triple - -% TODO example: -\begin{lstlisting}[style=java] - Triple sameL(List l) - Triple sameP(Pair l) - void triple(Triple tr){} - -Pair p ... -List l ... - -make(t) { return t; } -triple(make(sameP(p))); -triple(make(sameL(l))); -\end{lstlisting} - -\begin{constraintset} -$ -\exptype{Triple}{\rwildcard{X}, \rwildcard{X}, \rwildcard{X}} \lessdot \ntv{t}, -\ntv{t} \lessdotCC \exptype{Triple}{\wtv{a}, \wtv{b}, \wtv{b}}, \\ -(\textit{This constraint is added later: } \exptype{Triple}{\rwildcard{X}, \rwildcard{Y}, \rwildcard{Y}} \lessdot \ntv{t}) -$ -% Triple <. t -% ( Triple <. t ) <- this constraint is added later -% t <. Triple - -% t =. x.Triple -\end{constraintset} - -%TODO -% The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards} -% and \cite{WildcardsNeedWitnessProtection}. - -% \subsection{Capture Conversion} -% The \texttt{let} statements in \TamedFJ{} act as capture conversion for wildcard types. - -% \begin{figure} -% \begin{minipage}{0.45\textwidth} -% \begin{lstlisting}[style=tfgj] -% List clone(List l); -% example(p){ -% return clone(p); -% } -% \end{lstlisting} -% \end{minipage}% -% \hfill -% \begin{minipage}{0.5\textwidth} -% \begin{lstlisting}[style=letfj] -% List clone(List l); -% (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p) = -% let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in -% clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*); -% \end{lstlisting} -% \end{minipage} -% \caption{Type inference adding capture conversion}\label{fig:addingLetExample} -% \end{figure} - -% 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}}$. -% 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 -% ($\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 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. -% 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. - -% 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}}$, -% which leads to: -% \begin{verbatim} -% List example(List p){ -% return clone(p); -% } -% \end{verbatim} - -% But by substituting $\tv{p} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in the constraint -% $\tv{p} \lessdotCC \exptype{List}{\wtv{x}}$ leads to -% $\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: -% $\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}})$ - -% Inside the let statement the variable \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ - - -% This spawns additional problems. - -% \begin{figure} -% \begin{minipage}{0.45\textwidth} -% \begin{verbatim} -% List clone(List l){...} - -% example(p){ -% return clone(p); -% } -% \end{verbatim} -% \end{minipage}% -% \hfill -% \begin{minipage}{0.35\textwidth} -% \begin{constraintset} -% \textbf{Constraints:}\\ -% $ -% \tv{p} \lessdotCC \exptype{List}{\wtv{x}}, \\ -% \tv{p} \lessdot \tv{r}, \\ -% \tv{p} \lessdot \type{Object}, -% \tv{r} \lessdot \type{Object} -% $ -% \end{constraintset} -% \end{minipage} - -% \caption{Type inference example}\label{fig:ccExample} -% \end{figure} - -% In addition with free variables this leads to unwanted behaviour. -% Take the constraint -% $\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}$ -% we get -% $\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$. -% Which is correct if we apply capture conversion to the left side: -% $\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 -% type solution due to: -% $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \nless: \exptype{List}{\rwildcard{X}}$ -% The reason for this is the \texttt{S-Exists} rule's premise -% $\text{dom}(\Delta') \cap \text{fv}(\exptype{List}{\rwildcard{X}}) = \emptyset$. - -% 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. \ No newline at end of file diff --git a/martin.bib b/martin.bib index 64db956..e07bf3e 100644 --- a/martin.bib +++ b/martin.bib @@ -558,3 +558,14 @@ Computing Concepts}, url = {https://www.dhbw-stuttgart.de/forschung-transfer/technik/schriftenreihe-insights} } +@article{wells1999typability, + title={Typability and type checking in System F are equivalent and undecidable}, + author={Wells, Joe B}, + journal={Annals of Pure and Applied Logic}, + volume={98}, + number={1-3}, + pages={111--156}, + year={1999}, + publisher={Elsevier} +} + diff --git a/tRules.tex b/tRules.tex index 3b04f7e..4cb2230 100644 --- a/tRules.tex +++ b/tRules.tex @@ -1,34 +1,46 @@ -\section{Syntax and Typing}\label{sec:tifj} -The input syntax for our algorithm is shown in figure \ref{fig:syntax} +\section{\TamedFJ{}}\label{sec:tifj} +%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. +The syntax is shown in figure \ref{fig:syntax} and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}. -Our calculus is a subset of the calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection} -with the exception that type annotations are optional in our calculus. +Method parameters and return types are optional. +We still require 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 type inferred 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:syntax} with optional type annotations highlighted in yellow. +It is possible to exclude all optional types. +\TamedFJ{} is a subset of the calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection}. +%The language is designed to showcase type inference involving existential types. +The idea is for our type inference algorithm to calculate all missing types and output a fully and correctly typed \TamedFJ{} program, +which by default is also a correct Featherweight Java program (see chapter \ref{sec:soundness}). -Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm. -The input language is designed to showcase type inference involving existential types. -Method call rule T-Call is the most interesting part, because it emulates the behaviour of a Java method call, -where existential types are implicitly \textit{opened} and \textit{closed}. - -Example: %TODO -\begin{verbatim} -class List { - A head; - List tail; - - add(v) = new List(v, this); -} -\end{verbatim} - -%The rules depicted here are type inference rules. It is not possible to derive a distinct typing from a given input program. - -%The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}. -%and is solely used for examples. -The calculus does not include method overriding for simplicity reasons. +\noindent +\textit{Notes:} +\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 proofing completeness like in \cite{TIforFGJ} the calculus +needs to be restricted in that regard. +Our algorithm is not complete (see discussion in chapter \ref{sec:completeness}) and without the respective proof we can keep the \TamedFJ{} calculus as simple as possible +and as close to it's Featherweight Java correspondent \cite{WildcardsNeedWitnessProtection} as possible. +Our soundness proof works either way. +\end{itemize} %Additional features like overriding methods and method overloading can be added by copying the respective parts from there. %Additional features can be easily added by generating the respective constraints (Plümicke hier zitieren) @@ -40,200 +52,37 @@ Additional language constructs can be added by implementing the respective const % on overriding methods, because their type is already determined. % Allowing overriding therefore has no implication on our type inference algorithm. -The syntax forces every expression to undergo a capture conversion before it can be used as a method argument. -Even variables have to be catched by a let statement first. -This behaviour emulates Java's implicit capture conversion. +% 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. +\newcommand{\highlight}[1]{\begingroup\fboxsep=0pt\colorbox{yellow}{$\displaystyle #1$}\endgroup} \begin{figure} +\par\noindent\rule{\textwidth}{0.4pt} +\center $ \begin{array}{lrcl} -\hline +%\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{\expr{x}}) \set{ \texttt{return}\ t;} \\ -\text{Terms} & t & ::= & \expr{x} \\ -& & \ \ | & \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}_c}) \\ -& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \expr{x}_c.f \\ -& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \expr{x}_c.\texttt{m}(\overline{\expr{x}_c}) \\ -& & \ \ | & t \elvis{} t \\ +\text{Method declarations} & \texttt{M} & ::= & \highlight{\generics{\overline{\type{X} \triangleleft \type{N}}}}\ \highlight{\type{T}}\ \texttt{m}(\overline{\highlight{\type{T}}\ \expr{x}}) \{ \texttt{return} \ \expr{e}; \} \\ +\text{Terms} & \expr{e} & ::= & \expr{x} \\ +& & \ \ | & \texttt{new} \ \type{C}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\ +& & \ \ | & \expr{e}.f\\ +& & \ \ | & \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 +%\hline \end{array} $ -\caption{\TamedFJ{} Syntax}\label{fig:syntax} +\par\noindent\rule{\textwidth}{0.4pt} +\caption{Input Syntax with optional type annotations}\label{fig:syntax} \end{figure} -% \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{\expr{x}}) = t \\ -% \text{Values} & v & ::= & \expr{x} \\ -% \text{Terms} & t & ::= & v \\ -% & & \ \ | & \texttt{let} \ \expr{x} = \texttt{new} \ \type{C}(\overline{v}) \ \texttt{in} \ t \\ -% & & \ \ | & \texttt{let} \ \expr{x} = v.f \ \texttt{in} \ t \\ -% & & \ \ | & \texttt{let} \ \expr{x} = v.\texttt{m}(\overline{v}) \ \texttt{in} \ t \\ -% & & \ \ | & \texttt{let} \ \expr{x} = v \elvis{} v \ \texttt{in} \ t \\ -% \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\ -% \hline -% \end{array} -% $ -% \caption{Input Syntax}\label{fig:syntax} -% \end{figure} - -% \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{\expr{x}}) = t \\ -% \text{Terms} & t & ::= & \expr{x} \\ -% & & \ \ | & \texttt{let} \ \expr{x} = t \ \texttt{in} \ t \\ -% & & \ \ | & \expr{x}.f \\ -% & & \ \ | & \expr{x}.\texttt{m}(\overline{\expr{x}}) \\ -% & & \ \ | & t \elvis{} t \\ -% \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\ -% \hline -% \end{array} -% $ -% \caption{Input Syntax}\label{fig:syntax} -% \end{figure} - - -% \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}) = 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:syntax} -% \end{figure} - -\subsection{ANF transformation}\label{sec:anfTransformation} -\newcommand{\anf}[1]{\ensuremath{\tau}(#1)} -%https://en.wikipedia.org/wiki/A-normal_form) -Featherweight Java's syntax involves no \texttt{let} statement -and terms can be nested freely. -This is similar to Java's syntax. -To convert it to \TamedFJ{} additional let statements have to be added. -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:}\\ -\noindent -\begin{minipage}{0.45\textwidth} -\begin{lstlisting}[style=fgj,caption=Featherweight Java] -m(l, v){ - return l.add(v); -} -\end{lstlisting} - \end{minipage}% - \hfill - \begin{minipage}{0.5\textwidth} -\begin{lstlisting}[style=tfgj,caption=\TamedFJ{} representation] -m(l, v) = - let x1 = l in - let x2 = v in x1.add(x2) -\end{lstlisting} -\end{minipage} - - -% $ -% \begin{array}{|lrcl|l} -% \hline -% & & & \textbf{Featherweight Java Terms}\\ -% \text{Terms} & t & ::= -% & \expr{x} -% \\ -% & & \ \ | -% & \texttt{new} \ \type{C}(\overline{t}) -% \\ -% & & \ \ | -% & t.f -% \\ -% & & \ \ | -% & t.\texttt{m}(\overline{t}) -% \\ -% & & \ \ | -% & t \elvis{} t\\ -% % -% \hline -% \end{array} -% $ - -\begin{figure} - \begin{center} -$\begin{array}{lrcl} -%\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{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_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2} -\end{array}$ -\end{center} -\caption{ANF Transformation}\label{fig:anfTransformation} -\end{figure} - -% $ -% \begin{array}{lrcl|l} -% \hline -% & & & \textbf{Featherweight Java} & \textbf{A-Normal form} \\ -% \text{Terms} & t & ::= -% & \expr{x} -% & \expr{x} -% \\ -% & & \ \ | -% & \texttt{new} \ \type{C}(\overline{t}) -% & \texttt{let}\ \overline{x} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{x}) -% \\ -% & & \ \ | -% & t.f -% & \texttt{let}\ x = t \ \texttt{in}\ x.f -% \\ -% & & \ \ | -% & t.\texttt{m}(\overline{t}) -% & \texttt{let}\ x_1 = t \ \texttt{in}\ \texttt{let}\ \overline{x} = \overline{t} \ \texttt{in}\ x_1.\texttt{m}(\overline{x}) -% \\ -% & & \ \ | -% & t \elvis{} t -% & t \elvis{} t\\ -% % -% \hline -% \end{array} -% $ - - -% Each class type has a set of wildcard types $\overline{\Delta}$ attached to it. -% The type $\wctype{\overline{\Delta}}{C}{\ol{T}}$ defines a set of wildcards $\overline{\Delta}$, -% which can be used inside the type parameters $\ol{T}$. - \begin{figure}[tp] \begin{center} $\begin{array}{l} @@ -500,9 +349,10 @@ $\begin{array}{l} $\begin{array}{l} \typerule{T-Method}\\ \begin{array}{@{}c} - (\type{T'},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad - \triangle' = \overline{\type{Y} : \bot .. \type{P}} \quad \quad - \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\ + \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\ldots} \quad \quad + \generics{\ol{Y \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m}) \quad \quad + \triangle' = \overline{\type{Y} : \bot .. \type{P}} \\ + \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \quad \quad \text{dom}(\triangle) = \ol{X} \quad \quad %\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \ \{ \ldots \} \\ \mathtt{\Pi} | \triangle, \triangle' | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \quad \quad @@ -510,37 +360,33 @@ $\begin{array}{l} \\ \hline \vspace*{-0.3cm}\\ - \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \text{ in C with } \generics{\ol{Y \triangleleft P}} + \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) \set{ \texttt{return}\ \texttt{e}; } \ \ok \ \text{in C} \end{array} \end{array}$ \\[1em] $\begin{array}{l} \typerule{T-Class}\\ \begin{array}{@{}c} - \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}} \\ - \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} } \\ + %\forall \texttt{m} \in \ol{M} : \mathtt{\Pi}(\texttt{m}) = \generics{\ol{X \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \\ \triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad \triangle \vdash \ol{U}, \ol{T}, \type{N} \ \ok \quad \quad - \mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C with} \ \generics{\ol{Y \triangleleft P}} + \mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C} \\ \hline \vspace*{-0.3cm}\\ - \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \} : \mathtt{\Pi}'' + \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \} : \mathtt{\Pi} \end{array} \end{array}$ -\\[1em] +%\\[1em] +\hfill $\begin{array}{l} \typerule{T-Program}\\ \begin{array}{@{}c} - \emptyset \vdash \texttt{L}_1 : \mathtt{\Pi}_1 \quad \quad - \mathtt{\Pi}_1 \vdash \texttt{L}_2 : \mathtt{\Pi}_1 \quad \quad - \ldots \quad \quad - \mathtt{\Pi}_{n-1} \vdash \texttt{L}_n : \mathtt{\Pi}_n \quad \quad + \mathtt{\Pi} = \overline{\texttt{m} : \generics{\ol{X \triangleleft \type{N}}}\ol{T} \to \type{T}} \\ \hline \vspace*{-0.3cm}\\ - \vdash \ol{L} : \mathtt{\Pi}_n + \overline{D : \mathtt{\Pi}} \end{array} \end{array}$ \end{center} diff --git a/unify.tex b/unify.tex index 1d7ccc9..86e72f4 100644 --- a/unify.tex +++ b/unify.tex @@ -330,6 +330,13 @@ Otherwise proceed with step 3. %$\type{T} \lessdot \ntv{a}$ constraints have three and $\type{T} \lessdot \wtv{a}$ constraints have five possible transformations. +\textit{Hint:} +When implementing this step via backtracking +the rules \rulename{General} and \rulename{Super} should be tried first. +% is the Same rule really necessary? +The \rulename{Settle} and \rulename{Raise} rules should only be used when none of the rules in figure \ref{fig:step2-rules} can be applied. + + \item[Step 3:] Apply the rules in figure \ref{fig:cleanup-rules} exhaustively. \rulename{Ground} and \rulename{Flatten} deal with constraints containing free variables. @@ -648,7 +655,7 @@ Prepare, Capture, Reduce, Trim, Clear, Exclude, Adapt \rulename{Bot} & $ \begin{array}[c]{l} - \wildcardEnv \vdash C \cup \set{ \bot \lessdot_1 \type{T} } \\ + \wildcardEnv \vdash C \cup \set{ \bot \lessdot \type{T} } \\ \hline \vspace*{-0.4cm}\\ \wildcardEnv \vdash C @@ -658,7 +665,7 @@ Prepare, Capture, Reduce, Trim, Clear, Exclude, Adapt \rulename{Pit} $ \begin{array}[c]{l} - \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot_1 \bot } \\ + \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \bot } \\ \hline \vspace*{-0.4cm}\\ \wildcardEnv \vdash C \cup \set{ \tv{a} \doteq \bot } @@ -1081,23 +1088,28 @@ $\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_{in} % } % \end{array} % $ - \\\\ - \cdashline{1-2} \\ - \rulename{\generalizeRule{}W} %TODO: Change description for step 2! - & $ - \begin{array}[c]{l} - \wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \wtv{a}\\ - \hline - \wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \wtv{a}, - \wtv{a} \doteq \wctype{\overline{\wildcard{X}{\wtv{u}}{\wtv{l}}}}{C}{\overline{\rwildcard{X}}}, - %\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards - \overline{\wtv{u} \lessdot \type{S}} - } - \end{array} \quad \begin{array}[c]{l} - \texttt{class} \ \exptype{C}{\ol{X \triangleleft \type{S}}} \triangleleft \exptype{D}{\ol{N}} \\ - \text{fresh}\ \overline{\wildcard{X}{\wtv{u}}{\wtv{l}}} - \end{array} - $ + % \\\\ + % \cdashline{1-2} \\ + % \rulename{\generalizeRule{}W} %TODO: Change description for step 2! + % & $ + % \begin{array}[c]{l} + % \wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \wtv{a}\\ + % \hline + % \wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \wtv{a}, + % \wtv{a} \doteq \wctype{\overline{\wildcard{X}{\wtv{u}}{\wtv{l}}}}{C}{\overline{\rwildcard{X}}}, + % %\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards + % \overline{\wtv{u} \lessdot \type{S}} + % } + % \end{array} \quad \begin{array}[c]{l} + % \texttt{class} \ \exptype{C}{\ol{X \triangleleft \type{S}}} \triangleleft \exptype{D}{\ol{N}} \\ + % \text{fresh}\ \overline{\wildcard{X}{\wtv{u}}{\wtv{l}}} + % \end{array} + % $ + % %The idea behind the GeneralW rule is, that a constraint X.Pair <. a? can be resolved: + % % X.Pair <. Y,Z.Pair + % % X =. y, X =. z, y <. yu?, z <. zu?, yl? <. y, zl? <. z + % % X <. yu?, X <. zu?, yl? <. X, zl? <. X + % % ??? \end{tabular} } \end{center}