diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 46 |
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, |