diff options
author | David A. Madore <david+git@madore.org> | 2023-11-15 14:32:48 +0100 |
---|---|---|
committer | David A. Madore <david+git@madore.org> | 2023-11-15 14:32:48 +0100 |
commit | a231bd9587eefba7a4b6c51e3b5339a0320f87c3 (patch) | |
tree | 790688c98b707b143abf4977127d9f5712af8eab /transp-inf110-02-typage.tex | |
parent | 7e630cae17fbd8c7f3c056baab54a944bd1c8520 (diff) | |
download | inf110-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.tex | 35 |
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} |