From 10782eec65fcddacdfe7a6e1a960e947c3726f47 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sat, 16 Dec 2023 12:39:20 +0100
Subject: Description of the unification phase of Hindley-Milner.

---
 transp-inf110-02-typage.tex | 36 +++++++++++++++++++++++++++++++++++-
 1 file changed, 35 insertions(+), 1 deletion(-)

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
@@ -4856,6 +4856,40 @@ successivement les types et contraintes suivants :\quad
 $x:\eta_1$,\quad $xx:\eta_2$ avec $\eta_1 = (\eta_1 \to \eta_2)$,\quad
 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}
-- 
cgit v1.2.3