From 5d718f143bc8b11e257b1be3b2f42e4e5f5eb134 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Tue, 28 Nov 2023 10:15:10 +0100 Subject: Avoid speaking of type "constructors", a word which might cause confusion. --- transp-inf110-02-typage.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 7df864b..7b1f031 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -226,14 +226,14 @@ P.ex. la fonction « identité » $(\forall\mathtt{t})\; \mathtt{t} \bigskip -\itempoint \textbf{Constructeurs de types} = fabriquent un type à +\itempoint \textbf{Familles de types} = fabriquent un type à 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 +(produits, sommes, fonctions, familles…) à partir des types définis eux-mêmes. P.ex. $\texttt{Tree} = \texttt{List}~\texttt{Tree}$. @@ -362,7 +362,7 @@ $\texttt{Ref~Nat}$ = type d'une \alert{référence} vers un entier en Haskell, $\texttt{Char}$ = caractère = fonction de zéro argument renvoyant un caractère (fonction pure : toujours le même retour), mais $\texttt{IO~Char}$ = \alert{action} avec effets de bord renvoyant un -caractère ($\texttt{IO}$ est un constructeur de type appelé « monade » +caractère ($\texttt{IO}$ est une famille de type appelé « monade » I/O). \bigskip @@ -733,7 +733,7 @@ n'a aucune des trois, CoC a les trois) : polymorphisme paramétrique « explicitement quantifié » (p.ex. $\prod t.\; (t \rightarrow t)$) ; \item \textcolor{blue}{types pouvant dépendre de types}, ou - constructeurs de types ; + familles de types ; \item \textcolor{blue}{types pouvant dépendre de termes}, ou « types dépendants », correspondant côté logique à la quantification sur les individus. -- cgit v1.2.3