summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-11-14 18:51:29 +0100
committerDavid A. Madore <david+git@madore.org>2023-11-14 18:51:29 +0100
commita50ca41e03717aeed2ac590857a06c320dd702b6 (patch)
tree20958d4f08d2d626596116e8ef31e3fe8e3e6434
parent0a651f9b6c0a2f1c1a8f3b74555b77086d10a768 (diff)
downloadinf110-lfi-a50ca41e03717aeed2ac590857a06c320dd702b6.tar.gz
inf110-lfi-a50ca41e03717aeed2ac590857a06c320dd702b6.tar.bz2
inf110-lfi-a50ca41e03717aeed2ac590857a06c320dd702b6.zip
Generalities about polymorphism.
-rw-r--r--transp-inf110-02-typage.tex78
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}
%