Commit a0b39865 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

add some explanations in the appendix

parent ddb415d7
...@@ -876,7 +876,12 @@ ...@@ -876,7 +876,12 @@
\subsection{New algorithmic type system with type schemes} \subsection{New algorithmic type system with type schemes}
TODO: Why do we introduce type schemes? As explained in TODO, we introduce for the proofs the notion of \emph{types schemes}
and we define a new (more powerful) algorithmic type system that uses them.
It allows us to have a stronger (but still partial) completeness theorem.
The proofs for the algorithmic type system presented in \ref{sec:algorules} can be derived
from the proofs of this section (see section \ref{sec:proofs_algorithmic_without_ts}).
\subsubsection{Type schemes} \subsubsection{Type schemes}
...@@ -1735,7 +1740,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}. ...@@ -1735,7 +1740,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
We can prove it by induction over the structure of $e_+$. We can prove it by induction over the structure of $e_+$.
The main idea of this proof is that, as $e_+$ is a positive expression, the rule \Rule{Abs-} is not needed anymore The main idea of this proof is that, as $e_+$ is a positive expression, the rule \Rule{Abs-} is not needed anymore
because the negative part of functional types (i.e. the $N_i$ part of their DNF) become useless: because the negative part of functional types (i.e. the $N_i$ part of their DNF) becomes useless:
\begin{itemize} \begin{itemize}
\item When typing an application $e_1 e_2$, the negative part of the type of $e_1$ \item When typing an application $e_1 e_2$, the negative part of the type of $e_1$
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment