Description of the unification phase of Hindley-Milner.

1 files changed, 35 insertions, 1 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index b0d3028..653b8bb 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -4796,7 +4796,7 @@ autres se dérivent par substitution.
 \end{frame}
 %
 \begin{frame}
-\frametitle{Collection des contraintes}
+\frametitle{Première phase : collection des contraintes}
 
 La première phase de l'algorithme de H-M fonctionne comme la
 vérification de type du $\lambda$CST
@@ -4858,4 +4858,38 @@ et on renvoie finalement le type $\eta_1 \to \eta_2$.
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Seconde phase : résolution des contraintes}
+
+L'algorithme d'\textbf{unification} prend en entrée un ensemble
+$\mathscr{C}$ de contraintes (équations $\zeta_1 = \zeta_2$ avec
+$\zeta_1,\zeta_2$ deux types) et renvoie une \textbf{substitution} des
+variables de type ($\{\eta \mapsto \tau\}$ avec $\eta$ des variables
+de type et $\tau$ des types \alert{ne faisant pas intervenir} les
+variables substituées) qui vérifie les contraintes, ou « échec » :
+
+\medskip
+
+\itempoint Si $\mathscr{C}$ est vide, renvoyer la substitution vide.
+
+\smallskip
+
+\itempoint Sinon, soit $\zeta_1 = \zeta_2$ une contrainte, et
+$\mathscr{C}' := \mathscr{C} \setminus \{(\zeta_1 = \zeta_2)\}$ le
+reste des contraintes :
+\begin{itemize}
+\item si $\zeta_1 = \zeta_2$ déjà, unifier $\mathscr{C}'$,
+\item si $\zeta_1$ est une \alert{variable} de type $\eta$ :
+  \alert{si} $\zeta_2$ ne fait pas intervenir $\eta$, ajouter $\eta
+  \mapsto \zeta_2$ à la substitution, et unifier $\mathscr{C}'$ où
+  $\eta$ est remplacé par $\zeta_2$ ; \alert{sinon}, \alert{échouer}
+  (« type récursif ») ;
+\item si $\zeta_2$ est une variable de type : symétriquement ;
+\item sinon, $\zeta_1 = (\xi_1 \to \chi_1)$ et $\zeta_2 = (\xi_2 \to
+  \chi_2)$ : unifier $\mathscr{C}'' := \mathscr{C}' \cup \{(\xi_1 =
+  \xi_2), (\chi_1 = \chi_2)\}$.
+\end{itemize}
+
+\end{frame}
+%
 \end{document}