Basic set of slides on typing.

1 files changed, 296 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
new file mode 100644
index 0000000..7ee04fe
--- /dev/null
+++ b/transp-inf110-02-typage.tex
@@ -0,0 +1,296 @@
+%% This is a LaTeX document.  Hey, Emacs, -*- latex -*- , get it?
+\documentclass[mathserif,a4paper,aspectratio=169]{beamer}
+%\documentclass[a4paper]{article}
+%\usepackage[envcountsect,noxcolor]{beamerarticle}
+\usepackage[shorthands=off,french]{babel}
+\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{lmodern}
+\DeclareUnicodeCharacter{00A0}{~}
+\DeclareUnicodeCharacter{2026}{...}
+\DeclareUnicodeCharacter{1E25}{\d{h}}
+% Beamer theme:
+\usetheme{Goettingen}
+%\usecolortheme{albatross}
+%\usecolortheme{lily}
+%\setbeamercovered{transparent}
+% A tribute to the worthy AMS:
+\usepackage{amsmath}
+\usepackage{amsfonts}
+\usepackage{amssymb}
+\usepackage{amsthm}
+%
+\usepackage{mathrsfs}
+%
+\usepackage{graphicx}
+\usepackage{tikz}
+\usetikzlibrary{arrows,automata,calc}
+%
+\newcommand{\itempoint}{\strut\hbox{\color{beamerstructure}\donotcoloroutermaths$\blacktriangleright$}\nobreak\hskip.5em plus.5em\relax}
+\renewcommand{\thefootnote}{\textdagger}
+\newcommand{\dbllangle}{\mathopen{\langle\!\langle}}
+\newcommand{\dblrangle}{\mathclose{\rangle\!\rangle}}
+%
+%
+%
+\title{Typage simple}
+\subtitle{INF110 (Logique et Fondements de l'Informatique)}
+\author[David Madore]{David A. Madore\\
+{\footnotesize Télécom Paris}\\
+\texttt{david.madore@enst.fr}}
+\date{2023–2024}
+\mode<presentation>{%
+\beamertemplatenavigationsymbolsempty
+\usenavigationsymbolstemplate{\vbox{\hbox{\footnotesize\hyperlinkslideprev{$\leftarrow$}\insertframenumber/\inserttotalframenumber\hyperlinkslidenext{$\rightarrow$}}}}
+}
+\setbeamercolor{myhighlight}{fg=black,bg=white!90!green}
+\begin{document}
+\mode<article>{\maketitle}
+%
+\setlength\abovedisplayskip{2pt plus 2pt minus 2pt}
+\setlength\belowdisplayskip{2pt plus 2pt minus 2pt}
+%
+\begin{frame}
+\titlepage
+{\footnotesize\center{\url{http://perso.enst.fr/madore/inf110/transp-inf110.pdf}}\par}
+{\tiny
+\immediate\write18{sh ./vc > vcline.tex}
+\begin{center}
+Git: \input{vcline.tex}
+\end{center}
+\immediate\write18{echo ' (stale)' >> vcline.tex}
+\par}
+\end{frame}
+%
+\section*{Plan}
+\begin{frame}
+\frametitle{Plan}
+\tableofcontents
+\end{frame}
+%
+\section{Généralités sur le typage}
+\begin{frame}
+\frametitle{Qu'est-ce que le typage ?}
+
+{\footnotesize Philosophie opposée du « codage de Gödel » en
+  calculabilité, lequel représente toute donnée finie par un
+  entier.\par}
+
+\medskip
+
+\itempoint Informellement, un \textbf{système de typage} est une façon
+d'affecter à toute \alert{expression} et/ou \alert{valeur} manipulée
+par un langage informatique un \textbf{type} qui contraint son usage
+{\footnotesize (p.ex., « entier », « fonction », « chaîne de
+  caractères »)}.
+
+\medskip
+
+\textbf{Buts :}
+\begin{itemize}
+\item attraper plus tôt des \textbf{erreurs de programmation}
+  {\footnotesize (« ajouter un entier et une chaîne de caractères »
+    est probablement une erreur, ou demande une conversion
+    explicite)},
+\item éviter des \textbf{plantages ou problèmes de sécurité}
+  {\footnotesize (exécution d'un entier)},
+\item garantir certaines \textbf{propriétés du comportement} des
+  programmes ($\rightarrow$ analyse statique), forcément de façon
+  limitée (cf. théorème de Rice), p.ex., la \alert{terminaison},
+\item aider à l'\textbf{optimisation} {\footnotesize (fonction pure :
+  sans effet de bord)}.
+\end{itemize}
+
+\medskip
+
+{\footnotesize Cf. systèmes d'unités (homogénéité) en physique.\par}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Variétés de typage}
+
+Il y a autant de systèmes de typage que de langages de programmation !
+
+\medskip
+
+\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}
+
+\medskip
+
+\itempoint Typage \textbf{inféré} par le langage ou \textbf{annoté}
+par le programmeur.
+
+{\footnotesize Type = promesse donnée par le langage au
+  programmeur ou par le programmeur au langage ?\par}
+
+\medskip
+
+\itempoint Typage « sûr » ou partiel/contournable (\textit{cast} de
+la valeur, manipulation de la représentation mémoire, suppression ou
+report à l'exécution de vérification).
+
+\medskip
+
+\itempoint Typage superficiel {\footnotesize (« ceci est une liste »)}
+ou complexe {\footnotesize (« ceci est une liste d'entiers »)}.
+
+\medskip
+
+\itempoint Diverses annotations possibles {\footnotesize (« cette
+  fonction est pure », « soulève une exception »)}.
+
+\medskip
+
+\itempoint Liens avec les mécanismes de sécurité (qui peut faire
+quoi ?), de gestion de la mémoire (système de typage linéaire),
+l'évaluation (exceptions), la mutabilité.
+
+\medskip
+
+\itempoint Les types sont-ils citoyens de première classe
+           {\footnotesize (:= manipulables dans le langage)} ?
+
+{\footnotesize Juvénal : « Quis custodiet ipsos custodes? » Quel est
+  le type des types eux-mêmes ?\par}
+
+\end{frame}
+%
+\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
+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
+d'un entier et d'un booléen.
+
+\smallskip
+
+Composantes éventuellement nommées $\rightarrow$ structures
+(= enregistrements).
+
+\smallskip
+
+Produit vide = type trivial, $\mathtt{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,
+avec un \alert{sélecteur} de cas.
+
+\smallskip
+
+Cas particulier : $\mathtt{Unit} + \cdots + \mathtt{Unit}$ = type
+« énumération » (pur sélecteur).
+
+\smallskip
+
+Somme vide = type inhabité (impossible : aucune valeur).
+
+\bigskip
+
+\itempoint Types \textbf{fonctions} (= exponentielles).
+P.ex. $\mathtt{Nat} \rightarrow \mathtt{Bool}$.
+
+\bigskip
+
+\itempoint Types \textbf{listes}.  P.ex. $\mathtt{List}~\mathtt{Nat}$
+= type des listes d'entiers.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Quelques fonctionnalités fréquentes}
+
+\itempoint \textbf{Sous-typage} = les valeurs d'un type sont
+automatiquement des valeurs possibles d'un autre.
+
+\bigskip
+
+\itempoint \textbf{Polymorphisme} = utilisation de plusieurs types
+possibles, voire de n'importe quel type (cf. transp. suivant).
+P.ex. la fonction « identité » $(\forall\mathtt{t})\; \mathtt{t}
+\rightarrow \mathtt{t}$.
+
+\bigskip
+
+\itempoint \textbf{Constructeurs de types} = fabriquent un type à
+partir d'un (ou plusieurs) autres.  P.ex. $\mathtt{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}$.
+
+\bigskip
+
+\itempoint \textbf{Types dépendants} = un type à partir d'une valeur.
+P.ex. $k \mapsto \mathtt{Nat}^k$.
+
+\bigskip
+
+\itempoint \textbf{Types opaques} (abstraits, privés…) = types dont
+les valeurs sont cachées, l'usage est limité à une interface publique.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Quelques exemples}
+
+{\footnotesize Éviter les termes de typage « faible » et « fort », qui
+  veulent tout (ou rien) dire.\par}
+
+\medskip
+
+\itempoint Assembleur (langage machine) : aucun typage (tout est
+donnée binaire).
+
+{\footnotesize Idem : machine de Turing, fonctions générales
+  récursives (tout est entier), $\lambda$-calcul non typé (tout est
+  fonction).\par}
+
+\medskip
+
+\itempoint C : annoté, vérifié à la compilation (\emph{aucune}
+vérification à l'exécution), moyennement complexe et contournable
+(pointeurs génériques \texttt{void*}).
+
+\medskip
+
+\itempoint Python, JavaScript, Perl, Scheme, etc. : typage vérifié à
+l'exécution, superficiel.  Suffisant pour éviter les comportements
+indéfinis.
+
+\medskip
+
+\itempoint Java : annoté, mixte compilation/exécution (double
+vérification), initialement superficiel (listes non typées), puis
+introduction de « génériques » ($\rightarrow$ polymorphisme
+paramétrique) avec Java 5, puis diverses sortes d'inférence.
+
+\medskip
+
+\itempoint Rust : interaction avec la gestion de la mémoire
+($\approx$ typage linéaire).
+
+\medskip
+
+\itempoint OCaml, Haskell : langages fonctionnels avec système de
+typage très complexe (polymorphisme, constructeurs, types récursifs…)
+
+\end{frame}
+%
+\end{document}