From 22f53654a4a80c0a2e96a880a05ca695499e1a9b Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Wed, 15 Nov 2023 10:39:45 +0100
Subject: Tasks in a typing system.

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

(limited to 'transp-inf110-02-typage.tex')

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
@@ -295,6 +295,50 @@ fonction du type de son argument (connu à la compilation !).
   polymorphisme, voire la coercion (\textit{cast}).  Les limites de
   ces notions sont floues.\par}
 
+\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}
-- 
cgit v1.2.3