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

Start TYPE soundness

Browse Source
This commit is contained in:
Andreas Stadelmeier 2023-12-27 23:05:34 +01:00
parent ff8d309320
commit 18dd2325a6
2 changed files with 79 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

71
constraints.tex
View File

@ -1,4 +1,3 @@
\section{Constraint generation}
Our type inference algorithm is split into two parts.
A constraint generation step \textbf{TYPE} and a \unify{} step.
@ -248,7 +247,8 @@ C = \left\{ \begin{array}{l}
$\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as a free type variable.
%TODO: Do an example where wildcards are inserted and we need capture conversion
%\unify{} returns the solution $(\sigma = \set{ \tv{x} \to \type{String} })$
\unify{} returns the solution $(\sigma = \set{ \tv{x} \to \type{String} })$
% \\[1em]
% \noindent
@ -335,3 +335,70 @@ $\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as
\section{Result Generation}
If \unify{} returns atleast one type solution $(\Delta, \sigma)$
the last step of the type inference algorithm is to generate a typed class.
This section presents our type inference algorithm.
The algorithm is given method assumptions $\mv\Pi$ and applied to a
single class $\mv L$ at a time:
\begin{gather*}
\fjtypeinference(\mtypeEnvironment, \texttt{class}\ \exptype{C}{\ol{X}
\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \\
\quad \quad \begin{array}[t]{rll}
\textbf{let}\
(\overline{\methodAssumption}, \consSet) &= \fjtype{}(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \ldots \}) &
\text{// constraint generation}\\
{(\Delta, \sigma)} &= \unify{}(\consSet,\, \ol{X} <: \ol{N}) & \text{// constraint solving}\\
\generics{\ol{Y} \triangleleft \ol{S}} &= \set{ \type{Y} \triangleleft \type{S} \mid \wildcard{Y}{\type{P}}{\bot} \in \Delta} \\
\ol{M'} &= \set{ \generics{\ol{Y} \triangleleft \ol{S}}\ \sigma(\tv{a}) \ \texttt{m}(\ol{\sigma(\tv{a})\ x}) = \texttt{e} \mid (\mathtt{m}(\ol{x})\ = \mv e) \in \ol{M}, (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
%TODO: Describe whole algorithm (Insert types, try out every unify solution by backtracking (describe it as Non Deterministic algorithm))
\end{array}\\
\textbf{in}\ \texttt{class}\ \exptype{C}{\ol{X}
\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M'} \} \\
\textbf{in}\ \mtypeEnvironment \cup
\set{(\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \generics{\ol{Y} \triangleleft \ol{S}}\ \ol{\sigma(\tv{a})} \to \sigma(\tv{a})) \ |\ (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
% \fjtypeInsert(\overline{\methodAssumption}, (\sigma, \unifyGenerics{}) )
\end{gather*}
The overall algorithm is nondeterministic. The function $\unify{}$ may
return finitely many times as there may be multiple solutions for a constraint
set. A local solution for class $\mv C$ may not
be compatible with the constraints generated for a subsequent class. In this case, we have to backtrack to $\mv C$ and proceed to the next
local solution; if thats fail we have to backtrack further to an earlier class.
% \begin{gather*}
% \textbf{ApplyTypes}(\mtypeEnvironment, \texttt{class}\ \exptype{C}{\ol{X}
% \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \\
% \quad \quad \begin{array}[t]{rl}
% \textbf{let}\
% \ol{M'} &= \set{ \generics{\ol{Y} \triangleleft \ol{S}}\ \sigma(\tv{a}) \ \texttt{m}(\ol{\sigma(\tv{a})\ x}) = \texttt{e} \mid (\mathtt{m}(\ol{x})\ = \mv e) \in \ol{M}, (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
% \end{array}\\
% \textbf{in}\ \texttt{class}\ \exptype{C}{\ol{X}
% \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M'} \} \\
% \end{gather*}
% %TODO: Rules to create let statements
% % Input is type solution and untyped program.
% % Output is typed program
% % describe conversion for each expression
% Given a result $(\Delta, \sigma)$ and the type placeholders generated by $\TYPE{}$
% we can construct a \wildFJ{} program.
% %TODO: show soundness by comparing constraints and type rules
% % untyped expression | constraints | typed expression (making use of constraints and sigma)
% $\begin{array}{l|c|r}
% m(x) = e & r m(p x) = e & \Delta \sigma(r) m(\sigma(p) x) = |e| \\
% e \elvis{} e' \\
% e.m(\ol{e}) & (e:a).m(\ol{e:p}) & a <. T, p <. T & let x : sigma(a) = e in e.m(x); %TODO
% \end{array}$
% \begin{displaymath}
% \begin{array}[c]{l}
% \\
% \hline
% \vspace*{-0.4cm}\\
% \wildcardEnv
% \vdash C \cup \, \set{
% \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
% \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
% \end{array}
% \end{displaymath}

11
soundness.tex
View File

@ -1,6 +1,15 @@
\section{Soundness}
\begin{theorem}\label{testenv-theorem}
Type inference produces a correctly typed program.
\begin{description}
\item[If] $\fjtypeinference(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \mtypeEnvironment{}'$
\item[Then] $\texttt{class}\ \exptype{C}{\ol{X}
\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \} \text{ok}$,
with $\ol{M} = $
\end{description}
\end{theorem}
% %This lemma can be used to proof Normalize rule!
% \begin{lemma}\label{lemma:wildcardReplacement}