Typage statique - Définition

Problèmes

C'est ce dernier point qui est le plus délicat. Supposons une dérivation de Graphe : la classe Réseau spécialise Graphe, Routeur spécialise Nœud et Lien spécialise Arête.

En particulier, la méthode ajout_nœud est redéfinie dans Réseau :

       boolean ajout_nœud (Routeur r) { ... } //modélisation covariante conforme à l'intuition      

Considérons alors le code suivant :

       Réseau res = new Réseau;       Nœud n = new Nœud;       res.ajout_nœud (n); //Boum ! Le compilateur refuse ceci.      

En fait, pour garantir la sûreté du typage, il faut que le type des paramètres de la méthode ajout_nœud de Réseau soit un super-type du paramètre de la méthode ajout_nœud de Graphe.

De façon schématique :

Soient des classes A et B telles que B < A (« B spécialise A ») et B <: A (« B est un sous-type de A »); une méthode m(A) de type fonctionnel u→t définie sur A. Si B redéfinit m, alors le type de m(B) est u'→t' tels que u' <: u et t <: t', ce qui implique que u' < u et t < t'.

En d'autres termes, la redéfinition de méthode a pour corollaire la *covariance* du type de retour (ce type varie dans le même sens que B < A) et la *contravariance* du type des paramètres.

Inférence des types

Des langages à typage statique comme ML évitent en partie ces chausse-trappes en proposant un puissant mécanisme d'inférence de type : le compilateur devine le type des variables d'après les opérateurs utilisés par le programmeur.

Par exemple, si l'opérateur '+' est utilisé pour l'addition entière, le compilateur en déduira le type de ses arguments. Plus généralement, le moteur d'inférence de type essaie de déduire le type le plus général qui est un type valide pour le programme. Par exemple, le programme suivant ne fait aucune hypothèse sur le type de son argument :

       let identity x = x      

ML lui affectera le type : 'a -> 'a qui signifie qu'on peut utiliser la fonction identity avec un argument d'un type quelconque. Ainsi, les expressions "identity 0" et "identity 'a'" sont donc valides. On nomme polymorphisme ce typage général des programmes.

Il existe de nombreuses variantes du polymorphisme. Concilier inférence de types et polymorphisme avancé est une tâche complexe dans laquelle les langages Ocaml et Haskell brillent particulièrement. En Ocaml ou Haskell, l'inférence de type est capable d'inférer que le programme suivant :

       let double x = x + x      

ne peut être appliqué qu'à des arguments dont les valeurs sont compatibles avec l'opérateur +. Le type de double est alors en Ocaml int -> int et respectivement en Haskell Num a => a -> a.

Si les contraintes de typage ne sont pas satisfaisables alors le programmeur a fait une erreur de type.