diff --git a/TIforWildFJ.tex b/TIforWildFJ.tex index 1c97980..868efd8 100644 --- a/TIforWildFJ.tex +++ b/TIforWildFJ.tex @@ -123,7 +123,104 @@ $\begin{array}{rcl} \caption{Erasure} \label{fig:erasure} \end{figure} +% A constraint Pair <. a, then a has infinite possibilities: +% a =. X.Pair +% a =. X,Y.Pair +% a =. X.Pair,X> +% a =. X,Y.Pair,X> +% a =. X,Y.Pair,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 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 -> 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} diff --git a/constraints.tex b/constraints.tex index fa12ec1..57d7291 100644 --- a/constraints.tex +++ b/constraints.tex @@ -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} diff --git a/introduction.tex b/introduction.tex index 5a49689..b07d6a8 100644 --- a/introduction.tex +++ b/introduction.tex @@ -1,4 +1,9 @@ +%TODO: +% -Explain <: X^Y.C +% 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} diff --git a/tRules.tex b/tRules.tex index bea1cfb..8fefe08 100644 --- a/tRules.tex +++ b/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 as that and not convert to X,Y.Pair +% 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} diff --git a/unify.tex b/unify.tex index a874c3c..139f95d 100644 --- a/unify.tex +++ b/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 as class X extends List {} + % other way round: every class declaration comes in Delta_in + \\\\ \rulename{Bot} & $ \begin{array}[c]{l}