From 4eb7b1ce1981c7bb229e57d3238207171b1cf0c5 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Mon, 4 Mar 2024 15:37:21 +0100
Subject: [PATCH] =?UTF-8?q?=F0=9F=9B=A0=20work=20in=20progress?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 constraints.tex | 36 ++++++++++++++++++++++++++++++++++++
 soundness.tex   | 38 ++++++++++++++++++++++++++++++++++++++
 unify.tex       |  8 ++++++++
 3 files changed, 82 insertions(+)

diff --git a/constraints.tex b/constraints.tex
index 57d7291..92b412b 100644
--- a/constraints.tex
+++ b/constraints.tex
@@ -153,6 +153,42 @@ The set of method assumptions returned by the \textit{mtypes} function is used t
 
 There are two kinds of method calls.
 The ones to already typed methods and calls to untyped methods.
+
+LetFJ version: %TODO: or use the old version with \lessdotCC constraints. then there is no problem with \Delta'
+% or only use the \lessdotCC with X.C<X> and C<X> on both sides
+% what to do with ? <c X constraints? Just ignore them! they result in X <. X and can be ignored
+% generate a function which converts method types and parameter types to constraints of the form a <. X.C<X>, C<X> <. C<x>
+% add the free variables to \Delta' proof that they cannot escape the scope (they have to be treated differently than \Delta')
+\begin{displaymath}
+  \begin{array}{@{}l@{}l}
+      \typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}})) = \\
+      & \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}
+                    %TODO: add \ol{\wildcard{X}{\wtv{u}}{\wtv{l}}} to \Delta'
+                    [\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \wctype{\ol{\wildcard{X}{\wtv{u}}{\wtv{l}}}}{C}{\ol{X}},  \exptype{C}{\ol{X}} \lessdot \exptype{C}{\ol{X}},
+                    %[\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}},
+                    \overline{\tv{r}} \lessdot \ol{T},
+                    \ol{X} \lessdot \ol{N}, 
+                    \ol{Y} \lessdot \ol{N'} \}
+                  \end{array}\\
+            & \ |\ 
+            (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\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}, \, \overline{\wtv{b}} \text{ fresh} }
+        \end{array}\\
+      \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T})
+      \end{array}
+      \end{array}
+  \end{displaymath}
+
+Java version:
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
       \typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}})) = \\
diff --git a/soundness.tex b/soundness.tex
index 3171bbe..310a4ae 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -14,6 +14,44 @@ TODO: Beforehand we have to show that $\Delta \cup \overline{\Delta} | \Theta \v
 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)
+Free wildcards do not move inwards. We can show that every new type is either well-formed and therefore does not contain any free variables.
+Or it is a generic method call: is it possible to use any free wildcards here?
+let empty 
+
+<X> Box<X> empty()
+same(Box<?>, empty())
+let p1 : X.Box<X> = Box<?> in let 
+X.Box<X> <. Box<x> 
+Box<e> <. Box<x>
+
+boxin(empty()), Box2<?>
+
+Where can a problem arise? When we use free wildcards before they are freed.
+But we can always CC them first. Exception two types: X.Pair<X, y> and Y.Pair<x, Y>
+Here y = Y and x = X but 
+
+<X,Y> void same(Pair<X,Y> a, Pair<X,Y> b){}
+<X> Pair<?, X> left() { return null; }
+<X> Pair<X, ?> right() { return null; }
+
+<X> Box<X> id(Box<? extends Box<X>> x)
+here it could be beneficial to use a free wildcard as the parameter X to have it later
+Box<?> x = ...
+same(id(x), id(x)) <- this will be accepted by TI
+
+let left : X,Y.Pair<X,Y> = left() in
+ let right : Pair<X,Y> = right() in
+
+Compromise:
+- Generate constraints so that they comply with LetFJ
+- Propose a version which is close to Java
+
+Version for LetFJ:
+Is it still possible to do the capture conversion in form of constraints?
+X.C<X> <. C<x>
+T <. X.C<X>
+how to proof: X.C<X> ok
+
 
 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.
diff --git a/unify.tex b/unify.tex
index 139f95d..89e228b 100644
--- a/unify.tex
+++ b/unify.tex
@@ -1,3 +1,11 @@
+% TODO: unify changes
+% a? <. T can be deleted in the last step
+% remove lessdotCC constraints completely
+% delete wildcard tphs a? when needed
+% aswell ass free variables:
+% a <. T with fv(T) not empty and not in \Delta' must be removed by U = L
+% also in T <. T constraints no free variables are allowed on both sides
+% the algorithm only removes wildcards, never adds them
 
 \section{Unify}\label{sec:unify}