diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 78 |
1 files changed, 64 insertions, 14 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 7ee04fe..bd65942 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -163,14 +163,14 @@ l'évaluation (exceptions), la mutabilité. \begin{frame} \frametitle{Opérations de base sur les types} -En plus de types de base (p.ex. $\mathtt{Nat}$ = entiers, -$\mathtt{Bool}$ = booléens), les opérations suivantes sur les types +En plus de types de base (p.ex. $\texttt{Nat}$ = entiers, +$\texttt{Bool}$ = booléens), les opérations suivantes sur les types sont \emph{souvent} proposées par les systèmes de typage : \bigskip \itempoint Types \textbf{produits} (= paires, triplets, $k$-uplets). -P.ex. $\mathtt{Nat} \times \mathtt{Bool}$ = type des paires formées +P.ex. $\texttt{Nat} \times \texttt{Bool}$ = type des paires formées d'un entier et d'un booléen. \smallskip @@ -180,17 +180,17 @@ Composantes éventuellement nommées $\rightarrow$ structures \smallskip -Produit vide = type trivial, $\mathtt{Unit}$ (une seule valeur). +Produit vide = type trivial, $\texttt{Unit}$ (une seule valeur). \bigskip -\itempoint Types \textbf{sommes} (= unions). P.ex. $\mathtt{Nat} + -\mathtt{Bool}$ = type pouvant contenir un entier \emph{ou} un booléen, +\itempoint Types \textbf{sommes} (= unions). P.ex. $\texttt{Nat} + +\texttt{Bool}$ = type pouvant contenir un entier \emph{ou} un booléen, avec un \alert{sélecteur} de cas. \smallskip -Cas particulier : $\mathtt{Unit} + \cdots + \mathtt{Unit}$ = type +Cas particulier : $\texttt{Unit} + \cdots + \texttt{Unit}$ = type « énumération » (pur sélecteur). \smallskip @@ -200,11 +200,11 @@ Somme vide = type inhabité (impossible : aucune valeur). \bigskip \itempoint Types \textbf{fonctions} (= exponentielles). -P.ex. $\mathtt{Nat} \rightarrow \mathtt{Bool}$. +P.ex. $\texttt{Nat} \rightarrow \texttt{Bool}$. \bigskip -\itempoint Types \textbf{listes}. P.ex. $\mathtt{List}~\mathtt{Nat}$ +\itempoint Types \textbf{listes}. P.ex. $\texttt{List}~\texttt{Nat}$ = type des listes d'entiers. \end{frame} @@ -225,20 +225,20 @@ P.ex. la fonction « identité » $(\forall\mathtt{t})\; \mathtt{t} \bigskip \itempoint \textbf{Constructeurs de types} = fabriquent un type à -partir d'un (ou plusieurs) autres. P.ex. $\mathtt{List}$ (fabrique le +partir d'un (ou plusieurs) autres. P.ex. $\texttt{List}$ (fabrique le type « liste de $\mathtt{t}$ » à partir de $\mathtt{t}$). \bigskip \itempoint \textbf{Types récursifs} = construits par les opérateurs (produits, sommes, fonctions, constructeurs…) à partir des types -définis eux-mêmes. P.ex. $\mathtt{Tree} = -\mathtt{List}~\mathtt{Tree}$. +définis eux-mêmes. P.ex. $\texttt{Tree} = +\texttt{List}~\texttt{Tree}$. \bigskip \itempoint \textbf{Types dépendants} = un type à partir d'une valeur. -P.ex. $k \mapsto \mathtt{Nat}^k$. +P.ex. $k \mapsto \texttt{Nat}^k$. \bigskip @@ -248,6 +248,55 @@ les valeurs sont cachées, l'usage est limité à une interface publique. \end{frame} % \begin{frame} +\frametitle{Polymorphisme} + +On distingue deux (trois ?) sortes de polymorphismes : + +\medskip + +\itempoint Polymorphisme \textbf{paramétrique} (ou « génériques ») : +la même fonction \alert{s'applique à l'identique} à une donnée de +n'importe quel type. + +\smallskip + +Exemples : +\begin{itemize} +\item $\texttt{head} : (\forall\mathtt{t})\; \texttt{List}~\mathtt{t} \to \mathtt{t}$ (renvoie le premier élément d'une liste) +\item $\lambda xy.\langle x,y\rangle : + (\forall\mathtt{u},\mathtt{v})\; \mathtt{u} \to \mathtt{v} \to + \mathtt{u}\times \mathtt{v}$ (fabrique un couple) +\item $\lambda xyz.xz(yz) : + (\forall\mathtt{u},\mathtt{v},\mathtt{w})\; (\mathtt{u} \to + \mathtt{v} \to \mathtt{w}) \to (\mathtt{u} \to + \mathtt{v}) \to \mathtt{u} \to + \mathtt{w}$ +\end{itemize} + +\smallskip + +Pas seulement pour les fonctions ! $\texttt{[]} : +(\forall\mathtt{t})\; \texttt{List}~\mathtt{t}$ (liste vide) + +\smallskip + +{\footnotesize Et même : $\texttt{while~true~do~pass} : + (\forall\mathtt{t})\; \mathtt{t}$ (boule infinie)\par} + +\bigskip + +\itempoint Polymorphisme \textbf{ad hoc} (ou « surcharge » / +« \textit{overloading} ») : la fonction \alert{agit différemment} en +fonction du type de son argument. + +\bigskip + +{\footnotesize Le sous-typage est parfois considéré comme une forme de + polymorphisme. Les limites de ces notions sont floues.\par} + +\end{frame} +% +\begin{frame} \frametitle{Quelques exemples} {\footnotesize Éviter les termes de typage « faible » et « fort », qui @@ -289,7 +338,8 @@ paramétrique) avec Java 5, puis diverses sortes d'inférence. \medskip \itempoint OCaml, Haskell : langages fonctionnels avec système de -typage très complexe (polymorphisme, constructeurs, types récursifs…) +typage très complexe (polymor\textsuperscript{sme} paramétrique, types +récursifs… ; Haskell : +polymor\textsuperscript{sme} ad hoc) \end{frame} % |