summaryrefslogtreecommitdiffstats
path: root/transp-inf110-02-typage.tex
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-11-15 14:32:48 +0100
committerDavid A. Madore <david+git@madore.org>2023-11-15 14:32:48 +0100
commita231bd9587eefba7a4b6c51e3b5339a0320f87c3 (patch)
tree790688c98b707b143abf4977127d9f5712af8eab /transp-inf110-02-typage.tex
parent7e630cae17fbd8c7f3c056baab54a944bd1c8520 (diff)
downloadinf110-lfi-a231bd9587eefba7a4b6c51e3b5339a0320f87c3.tar.gz
inf110-lfi-a231bd9587eefba7a4b6c51e3b5339a0320f87c3.tar.bz2
inf110-lfi-a231bd9587eefba7a4b6c51e3b5339a0320f87c3.zip
Various curiosities.
(Thanks to Thierry Martinez for most of these suggestions.)
Diffstat (limited to 'transp-inf110-02-typage.tex')
-rw-r--r--transp-inf110-02-typage.tex35
1 files changed, 32 insertions, 3 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index c9269d5..af96c40 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -117,8 +117,8 @@ Il y a autant de systèmes de typage que de langages de programmation !
\itempoint Typage \textbf{statique} (à compilation) vs
\textbf{dynamique} (à exécution) ou mixte.
-{\footnotesize En général on préfère : erreur à la compilation $>$
- erreur à l'exécution $>$ plantage.\par}
+{\footnotesize Mixte = « graduel ». On préfère : erreur de
+ compilation $>$ erreur à l'exécution $>$ plantage.\par}
\medskip
@@ -200,7 +200,8 @@ Somme vide = type inhabité (impossible : aucune valeur).
\bigskip
\itempoint Types \textbf{fonctions} (= exponentielles).
-P.ex. $\texttt{Nat} \rightarrow \texttt{Bool}$.
+P.ex. $\texttt{Nat} \rightarrow \texttt{Bool}$ (f\textsuperscript{n}
+de $\texttt{Nat}$ vers $\texttt{Bool}$).
\bigskip
@@ -468,6 +469,34 @@ linéarité.
\end{frame}
%
\begin{frame}
+\frametitle{Quelques curiosités}
+
+\itempoint En F\#, les unités de mesure sont intégrées au système de
+typage, qui peut donc vérifier l'homogénéité physique.
+
+\bigskip
+
+\itempoint En Rust, le système de typage évite non seulement les
+fuites de mémoire mais aussi certains problèmes de concurrence
+(absence de \textit{race condition} sur les données).
+
+\bigskip
+
+\itempoint Certains langages spécialisés assurent, éventuellement en
+lien avec leur système de typage, des propriétés diverses de leurs
+programmes : terminaison garantie en temps polynomial (Bellantoni \&
+Cook 1992), voire constant (langage Usuba), validation XML (langage
+CDuce), absence de fuite d'information (langage Flow Caml), etc.
+
+\bigskip
+
+\itempoint En Idris, le système de typage est aussi un système de
+preuve (cf. Curry-Howard après) et permet de certifier des invariants
+quelconques d'un programme (p.ex., correction d'un algorithme de tri).
+
+\end{frame}
+%
+\begin{frame}
\label{typing-and-termination}
\frametitle{Typage et terminaison}