Tasks in a typing system.

1 files changed, 45 insertions, 1 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 3802414..9f53895 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -280,7 +280,7 @@ Pas seulement pour les fonctions !  $\texttt{[]} :
 
 \smallskip
 
-{\footnotesize Et même : $\texttt{while~true~do~pass} :
+{\footnotesize Et même : $\texttt{while~true~do~pass~done} :
   (\forall\mathtt{t})\; \mathtt{t}$ (boule infinie)\par}
 
 \bigskip
@@ -298,6 +298,50 @@ fonction du type de son argument (connu à la compilation !).
 \end{frame}
 %
 \begin{frame}
+\frametitle{Tâches d'un système de typage}
+
+\itempoint \textbf{Vérification} de type : vérifier qu'une expression
+\emph{annotée} a bien le type prétendu par les annotations.
+
+\bigskip
+
+\itempoint \textbf{Inférence} (« reconstruction » / « assignation »)
+de type : calculer le type de l'expression \alert{en l'absence
+  d'annotations} (ou avec annotations partielles).
+
+\medskip
+
+Algorithme important : \textbf{Hindley-Milner} (inférence de type dans
+les langages fonctionnels à polymorphisme paramétrique).  Utilisé
+dans OCaml, Haskell, etc.
+
+\medskip
+
+\textbf{N.B.} Dans un système de typage trop complexe, l'inférence
+(voire la vérification !) \textcolor{orange}{peut devenir indécidable}
+(notamment si types de première classe / dépendant de valeurs
+arbitraires à l'exécution).
+
+\bigskip
+
+{\footnotesize Rarement utile en informatique mais essentiel en
+  logique ($\cong$ recherche de preuves) :\par}
+
+\itempoint \textbf{Habitation} de type : trouver un \alert{terme}
+(=expression) ayant un type donné.
+
+{\footnotesize P.ex. : y a-t-il un terme de type
+  $(\forall\mathtt{p},\mathtt{q})\; ((\mathtt{p} \to \mathtt{q}) \to
+  \mathtt{p}) \to \mathtt{p}$ ?\par}
+
+{\footnotesize \textbf{N.B.} Dans les langages usuels, \alert{tous}
+  les types sont habités par une boucle infinie (« \texttt{while true
+    do pass done} » ou « \texttt{let rec f () = f () in f ()} »),
+  \alert{même} le type vide.\par}
+
+\end{frame}
+%
+\begin{frame}
 \frametitle{Utilisations du typage au-delà des valeurs stockées}
 
 \itempoint Annotation des \textbf{exceptions soulevables} (fréquent,