🛠 work in progress sync 🛠
This commit is contained in:
Andreas Stadelmeier
parent
132f34e2b9
commit
56b2cddf18
@ -123,7 +123,104 @@ $\begin{array}{rcl}
|
||||
\caption{Erasure} \label{fig:erasure}
|
||||
\end{figure}
|
||||
|
||||
% A constraint Pair<A,B> <. a, then a has infinite possibilities:
|
||||
% a =. X.Pair<X,X>
|
||||
% a =. X,Y.Pair<X,Y>
|
||||
% a =. X.Pair<Pair<X,X>,X>
|
||||
% a =. X,Y.Pair<Pair<X,Y>,X>
|
||||
% a =. X,Y.Pair<Pair<X,Y>,Y>
|
||||
|
||||
% There is no way to try out every single one of them.
|
||||
|
||||
Starting with the parameters of the method we gradually add every expression which only contains already captured expressions.
|
||||
|
||||
We have a typed expression
|
||||
|
||||
$|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} : \type{T} = \texttt{x in}$
|
||||
$|\texttt{e.f}, \texttt{r}| = |\texttt{e}, x| \texttt{let} r = x.\texttt{f} \ \texttt{in}$
|
||||
$|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} = \texttt{x in}$
|
||||
%TODO: write the transform rules:
|
||||
% |e.f, ret| = |e, r| let ret = r.f in
|
||||
% |x, ret| = let ret = x in
|
||||
% |e.m(e_), ret| = |e, r| |e_, a_| let ret = r.m(a_) in
|
||||
|
||||
Erasure functions:
|
||||
$|\texttt{x}| = \texttt{let r} : \wcNtype{\Delta}{N} = \texttt{x in r}$
|
||||
|
||||
$\texttt{x} \longmapsto \texttt{let}\ \texttt{xx} : \type{T} = \texttt{x in xx}$
|
||||
$\texttt{x}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in xf}$
|
||||
|
||||
$\begin{array}{l}
|
||||
\texttt{e} \longmapsto \texttt{let}\ \texttt{xe} : \type{T} = \texttt{e}' \ \texttt{in xe} \\
|
||||
\hline
|
||||
\vspace*{-0.4cm}\\
|
||||
\texttt{e}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in x}.f
|
||||
\end{array}$
|
||||
|
||||
Example:
|
||||
m(a, b) = a.m(b.f);
|
||||
|
||||
let xa = a in let xb = b in let xf = xb.f in let xm = xa.m(xf) in xm
|
||||
|
||||
% TODO: Now we have to proof that there is a LetFJ program for every TIFJ program!
|
||||
% |let xr : T = x1.m(x2) in e| = [x1.m(x2)/xr]|e|
|
||||
% |let xf : T = x1.f in e| = [x1.f/xf]|e|
|
||||
% |let xr : T = x in e| = [xr/x]|e|
|
||||
% |new C(x)| = new C(x)
|
||||
|
||||
% | let xr : T' = x in let xf : T = xr.f | = x.f
|
||||
|
||||
|
||||
% let x : T' = e' in x = |e|
|
||||
% ---------------------------------
|
||||
% | let xr : T' = x in let xf : T = xr.f | = x.f
|
||||
|
||||
|
||||
|
||||
% let x : T' = e' in x = |e|
|
||||
% -----------
|
||||
% =
|
||||
|
||||
We need a language which only has let statemnts and expressions on capture converted variables
|
||||
|
||||
The idea is to use wildcard placeholders inside the method. Also in the bounds of wildcards.
|
||||
This makes it possible to replace wildcards with free variables by setting upper and lower bound to that free variable.
|
||||
Free variables then can flow freely inside the method body.
|
||||
We have to show that a type solution implies that there is a possible transformation to a correct typed letFJ program.
|
||||
If there is a possible method type then there must exist a let configuration.
|
||||
% By starting with the parameter types and capturing them. Afterwards every capture creates free variables which are used inside
|
||||
% TODO: Proof!
|
||||
|
||||
The normal type placeholders represent denotable types.
|
||||
|
||||
%TODO: the type rules stay the same. We generate let statements in a fashion which removes all wildcard types.
|
||||
% what about wildcards getting returned by untyped methods? they can also be captured
|
||||
% TODO: try soundness proof on the original type rules!
|
||||
|
||||
Removing of extensive wildcards:
|
||||
$
|
||||
\wctype{\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{X}, \rwildcard{Y}}
|
||||
\lessdot \wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}} \\
|
||||
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \wtv{x}, \rwildcard{Y} \doteq \wtv{x} \\
|
||||
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \rwildcard{Y} \\
|
||||
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
|
||||
\implies \wctype{\wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{Y}, \rwildcard{Y}}, \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
|
||||
$
|
||||
|
||||
%e.f leads to constraints: r <c C<x> with return type equals the field type T.
|
||||
% T can contain free variables from r. but also it can be used in another constraint and get free variables from inner let statements
|
||||
% X.C<X> <c C<x> -> then T contains X variables
|
||||
|
||||
% let x1 = p1, x2 = p2 in
|
||||
% let r1 = x1 in let r2 = p2 in let f1 = r2.f in let r3 = x1 in let m2 = r3.m2() let ret = r1.m(f1,m2)
|
||||
% in ret
|
||||
|
||||
What about method invocation with no type yet. m2 :: a -> a
|
||||
they are also encased in let expression so the return type can be capture converted.
|
||||
Those methods and the parameter types of the current method are the only things not typed.
|
||||
All the other types cannot change their type. The captured wildcards can only flow from top to bottom.
|
||||
The return type of untyped methods has to be well-formed and cannot contain free variables.
|
||||
Therefore no free variables will flow into those types.
|
||||
|
||||
\input{tRules}
|
||||
|
||||
|
||||
@ -155,7 +155,7 @@ There are two kinds of method calls.
|
||||
The ones to already typed methods and calls to untyped methods.
|
||||
\begin{displaymath}
|
||||
\begin{array}{@{}l@{}l}
|
||||
\typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \wtv{a} ) = \\
|
||||
\typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}})) = \\
|
||||
& \begin{array}{ll}
|
||||
\textbf{let}
|
||||
& \tv{r}, \ol{\tv{r}} \text{ fresh} \\
|
||||
@ -165,9 +165,9 @@ The ones to already typed methods and calls to untyped methods.
|
||||
& \begin{array}{@{}l@{}l}
|
||||
\constraint = \orCons\set{ &
|
||||
\begin{array}[t]{l}
|
||||
%[\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \wctype{\ol{\wildcard{X}{\ntv{u}}{\ntv{l}}}}{C}{\ol{X}}, \wctype{\ol{\wildcard{X}{\ntv{u}}{\ntv{l}}}}{C}{\ol{X}} \lessdotCC \exptype{C}{\ol{X}},
|
||||
[\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}},
|
||||
\overline{\tv{r}} \lessdotCC \ol{T},
|
||||
\wtv{a} \doteq \type{T},
|
||||
\ol{X} \lessdot \ol{N},
|
||||
\ol{Y} \lessdot \ol{N'} \}
|
||||
\end{array}\\
|
||||
@ -176,7 +176,7 @@ The ones to already typed methods and calls to untyped methods.
|
||||
{\mtypeEnvironment}, \, |\ol{T}| = |\ol{e}|
|
||||
, \, \overline{\wtv{a}} \text{ fresh}, \, \overline{\wtv{b}} \text{ fresh} }
|
||||
\end{array}\\
|
||||
\mathbf{in} & \consSet_R \cup \overline{\consSet} \cup \constraint
|
||||
\mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T})
|
||||
\end{array}
|
||||
\end{array}
|
||||
\end{displaymath}
|
||||
|
||||
@ -1,4 +1,9 @@
|
||||
|
||||
%TODO:
|
||||
% -Explain <c
|
||||
% - Kapitel 1.2 + 1.3 ist noch zu komplex
|
||||
% - Constraints und Unifikation erklären, bevor Unifikation erwähnt wird
|
||||
|
||||
\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,
|
||||
|
||||
@ -2,6 +2,55 @@
|
||||
|
||||
\newcommand{\CC}{\text{CC}}
|
||||
|
||||
\begin{lemma}
|
||||
A sound TypelessFJ program is also sound under LetFJ type rules.
|
||||
\begin{description}
|
||||
\item[if:]
|
||||
$\Gamma | \Delta \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \ \text{in}\ C \text{with} \ \generics{\ol{Y \triangleleft P}}$
|
||||
\end{description}
|
||||
\end{lemma}
|
||||
|
||||
TODO: Beforehand we have to show that $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
|
||||
Here $\Delta$ does not contain every $\overline{\Delta}$ ever created.
|
||||
%what prevents a free variable to emerge in \Delta.N example Y^Object |- C<String> <: X^Y.C<X>
|
||||
% if the Y is later needed for an equals: same(id(x), x2)
|
||||
|
||||
If $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
|
||||
then there exists a $|\texttt{e}|$ with $\Delta | \Theta \vdash |\texttt{e}| : \wcNtype{\Delta'}{N}$ in LetFJ.
|
||||
This is possible by starting with the parameter types as the base case $\overline{\Delta} = \emptyset$.
|
||||
|
||||
|
||||
Each type $\wcNtype{\Delta'}{N}$ can only use wildcards already freed.
|
||||
|
||||
\textit{Proof} by structural induction.
|
||||
\begin{description}
|
||||
\item[$\texttt{e} = \texttt{x}$] $\Delta | \Theta \vdash \texttt{e} : \type{T} \mid \emptyset$
|
||||
$\Delta \vdash \type{T} \ \ok$ by \rulename{T-Method}
|
||||
and therefore $\Delta | \Theta \vdash \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$.
|
||||
|
||||
$|\texttt{x}, \texttt{e}| = \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$
|
||||
|
||||
\item[$\texttt{e} = \texttt{e}.\texttt{m}(\ol{e})$] there must be atleast one value in $\texttt{e}$ or $\ol{e}$
|
||||
\item[$\texttt{e}.f$] given let x : T = e' in x
|
||||
let x : T = e' in let xf = x.f in xf
|
||||
|
||||
Required:
|
||||
$ \Delta | \Theta \vdash e' : \type{T}_1$
|
||||
$\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$
|
||||
$\Delta, \Delta' | \Theta, x : \type{N} \vdash let xf = x.f in xf : \type{T}_2$
|
||||
|
||||
\end{description}
|
||||
|
||||
|
||||
\textbf{Proof:} Every program complying with our type rules can be converted to a correct LetFJ program.
|
||||
First we convert the program so that every wildcards used in an expression are in the $\Delta$ environment:
|
||||
m(p) = e => let xp = p in [xp/p]e
|
||||
x1.m(x2) => let xm = x1.m(x2=) in xm
|
||||
x.f => let xf = x.f in xf
|
||||
Then we have to proof there is never a wildcard used before it is declared.
|
||||
Wildcards are introduced by the capture conversions and nothing else.
|
||||
|
||||
|
||||
\begin{theorem}\label{testenv-theorem}
|
||||
Type inference produces a correctly typed program.
|
||||
\begin{description}
|
||||
|
||||
65
tRules.tex
65
tRules.tex
@ -214,6 +214,53 @@ $\begin{array}{l}
|
||||
\triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em] % TODO: we need subtyping for FJ without let statements. Problem is \Delta \vdash T witnessed. The \Delta here contains all the let statements beforehand.
|
||||
% TODO: maybe do a rule which adds let statements at any place! Goal: a program which Unify calculates a type for is also correct under our type laws and can be converted to LefFJ
|
||||
% motivation: do not use normal types as intermediate types. Keep a Pair<X,X> as that and not convert to X,Y.Pair<X,Y>
|
||||
% it is possible because the parameters of the method are normal types. we can start capture converting them
|
||||
% is it possible to say there exists any \Delta which makes the method body possible?
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Call}\\
|
||||
\begin{array}{@{}c}
|
||||
\Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\type{T}} \ \ok \quad \quad
|
||||
\Delta \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
|
||||
\generics{\ol{X \triangleleft U'}} \type{N} \to \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
|
||||
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
|
||||
\\
|
||||
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
|
||||
\Delta | \Gamma \vdash \texttt{e} : \type{T}_r \mid \Delta_G \quad \quad
|
||||
\Delta | \Gamma \vdash \ol{e} : \ol{T} \mid \overline{\Delta_G} \quad \quad
|
||||
\Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
|
||||
\Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
|
||||
\\
|
||||
\overline{\Delta_G}, \Delta_G, \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
|
||||
\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
|
||||
\overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T} \mid \Delta', \overline{\Delta}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Call}\\
|
||||
\begin{array}{@{}c}
|
||||
\Delta \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
|
||||
\generics{\ol{X \triangleleft U'}}\ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
|
||||
\Delta \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
|
||||
\\
|
||||
\Delta \vdash \ol{S} \ \ok \quad \quad
|
||||
\Delta | \Gamma \vdash \texttt{e}, \ol{e} : \ol{T} \mid \overline{\Delta'} \quad \quad
|
||||
\Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}} \quad \quad
|
||||
\Delta \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T} \mid \overline{\Delta}, \overline{\Delta'}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
% \Delta is not allowed to have wildcards depending on eachother. X^Y, Y^T for example
|
||||
\\[1em]
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Call}\\
|
||||
@ -278,6 +325,24 @@ $\begin{array}{l}
|
||||
|
||||
\begin{figure}
|
||||
\begin{center}
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Method}\\
|
||||
% TODO: do a rule that forbids variables in Delta which are not introduced by a capture conversion
|
||||
\begin{array}{@{}c}
|
||||
\exptype{C}{\ol{X}} \to \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 \\
|
||||
\text{dom}(\triangle) = \ol{X} \quad \quad
|
||||
%\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \ \{ \ldots \} \\
|
||||
\mathtt{\Pi} | \triangle, \triangle', \overline{\triangle} | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \mid \overline{\Delta} \quad \quad
|
||||
\triangle \vdash \type{S} <: \type{T}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \text{ in C with } \generics{\ol{Y \triangleleft P}}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Method}\\
|
||||
\begin{array}{@{}c}
|
||||
|
||||
14
unify.tex
14
unify.tex
@ -273,9 +273,21 @@ $
|
||||
\hline
|
||||
\vspace*{-0.4cm}\\
|
||||
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot \type{L} }
|
||||
\end{array} \quad \type{A} \notin \Delta_{in}
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
\rulename{Lower}
|
||||
& $
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot \type{A} } \\
|
||||
\hline
|
||||
\vspace*{-0.4cm}\\
|
||||
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot \type{L} }
|
||||
\end{array} \quad \type{A} \notin \Delta_{in}
|
||||
$ %TODO: a <. X with X in Delta_in => a =. X
|
||||
% other possibliity: is it allowed to see X extends List<X> as class X extends List<X> {}
|
||||
% other way round: every class declaration comes in Delta_in
|
||||
\\\\
|
||||
\rulename{Bot}
|
||||
& $
|
||||
\begin{array}[c]{l}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user