Type statique

Type statique

Typage statique

Sommaire

Définition

Le typage statique est une technique utilisée dans certains langages de programmation impératifs (C++, Java, Pascal, par exemple) pour associer à un symbole dénotant une variable le type de la valeur dénotée par la variable ; et dans certains langages de programmation fonctionnels (ML, Objective Caml, Haskell, etc.) pour associer à une fonction (un calcul) le type de son paramètre et le type de la valeur calculée.

Une telle association présente les bénéfices potentiels suivants :

  • un compilateur de langage à typage statique détecte les erreurs de types avant que le programme ne soit exécuté (on obtient ainsi la sûreté du typage),
  • le même compilateur peut tirer parti de l'information sur les types pour réaliser certaines optimisations du code objet,
  • enfin, puisque les types des objets manipulés sont connus, le compilateur peut éliminer cette information du code objet produit, avec pour principal avantage un gain de mémoire par rapport aux systèmes à typage dynamique.

Langages à objets et typage statique

(déplacer vers nouvel article : le problème de la covariance/contravariance)

Les langages à objets en particulier peuvent tirer parti du typage statique, afin de détecter avant l'exécution des erreurs de types (comme par exemple la tentative d'additionner un entier avec une chaîne de caractères). Toutefois, la sûreté du typage et la programmation orientée objet sont parfois en contradiction, parce que le typage sûr va à l'encontre de la modélisation « naturelle » du problème à résoudre avec l'approche objet (redéfinition contravariante du type des paramètres des méthodes pour la sûreté du typage vs. redéfinition covariante dans l'approche objet).

Pour éclaircir la dernière phrase, nous travaillons sur un exemple. Considérons en Java l'extrait de code suivant :

  Graphe mon_graphe = new Graphe ();
 
  Nœud n1, n2;
  n1 = new Nœud ();
  n2 = new Nœud ();
 
  Arête a = new Arête (n1, n2);
 
  mon_graphe.ajout_nœud (n1);
  mon_graphe.ajout_nœud (n2);
  mon_graphe.ajout_arête (a);

Quatre objets sont déclarés et instanciés, précédés de leur type (respectivement Graphe, Nœud, Arête). Si le programmeur essaye d'instancier mon_graphe avec le type Nœud, le compilateur le lui interdit car mon_graphe a été déclaré comme étant de type Graphe (contrôle sur le type de retour).

De même, si la méthode ajout_nœud () de la classe Graphe a été définie comme ceci :

 boolean ajout_nœud (Nœud n) { ... }

c'est-à-dire en spécifiant le type du paramètre reçu, le compilateur saura détecter une erreur d'appel (par exemple 'mon_graphe.ajout_nœud (a)') - (contrôle sur le type des paramètres).

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.

Résolution, autres difficultés

Des langages comme Java et C++ ont tranché en faveur de l'invariance des types de retour et des paramètres de méthodes bien que dans ces deux langages, les types de retour puissent être covariants.

Les besoins de la modélisation (covariance du type des paramètres) entraînent des astuces plus ou moins contestables pour la simuler dans ces langages : il faut combiner des opérateurs de *coercition descendante* (downcast) et la *surcharge statique* de méthodes pour y arriver.

Le langage de programmation Eiffel est le seul à admettre la redéfinition covariante du type des paramètres.

Dans *tous* les cas, le programmeur doit anticiper des erreurs de type à l'exécution, comme dans les langages à typage dynamique. En résumé, il faut admettre que « les erreurs de type sont dans la nature ». Par exemple, considérons :

  • classe Animal, méthode Mange (nourriture)
  • classe Vache, méthode Mange (de l'herbe)

Ce typage est (a priori) incorrect, et le compilateur refusera le programme car manifestement herbe <: nourriture (<: « est un sous-type de »). En pratique rien n'empêche qu'une instance de « Pâté d'alouettes » ne soit donné en paramètre à une instance de Vache. Corrigeons :

  • classe Vache, méthode Mange (de tout)

Le typage est donc « sûr », car nourriture <: tout. Donc à l'exécution, la vache peut recevoir des farines animales. La maladie de la vache folle est une erreur de type, garantie par la sûreté du typage...

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 satisfiables alors le programmeur a fait une erreur de type.

  • Portail de la programmation informatique Portail de la programmation informatique
Ce document provient de « Typage statique ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Type statique de Wikipédia en français (auteurs)

Игры ⚽ Поможем сделать НИР

Regardez d'autres dictionnaires:

  • Type de données — Type (informatique) Pour les articles homonymes, voir Type (homonymie). En programmation un type de données, ou simplement type, définit le genre de contenu d une donnée et les opérations pouvant être effectuées sur la variable correspondante.… …   Wikipédia en Français

  • Type 69/79 — Un Type 69II (base des Marines de Quantico) Caractéristiques de service Conflits Guerre Iran Irak (1980 1988) Guerre du Golfe (1990 1991) Opération libérat …   Wikipédia en Français

  • Type recursif — Type récursif Dans un langage de programmation, un type récursif ou type inductif est un type de données pour des valeurs qui contiennent d autres valeurs du même type. Un exemple est le type liste en Haskell : data List a = Nil | Cons a… …   Wikipédia en Français

  • Type (informatique) — Pour les articles homonymes, voir Type (homonymie). En programmation informatique, un type de donnée, ou simplement type, définit les valeurs que peut prendre une donnée, ainsi que les opérateurs qui peuvent lui être appliqués. Sommaire 1 Types… …   Wikipédia en Français

  • Statique du solide — Pour les articles homonymes, voir Statique. La statique du solide est la branche de la statique étudiant l équilibre des pièces dans un mécanisme. C est un maillon essentiel dans le dimensionnement des systèmes mécaniques réels. Sommaire 1… …   Wikipédia en Français

  • Type dynamique — Typage dynamique Tous les langages de programmation permettent, directement ou indirectement, de manipuler des valeurs. Généralement, c est par l entremise de variables, qui sont une association (on dit aussi une liaison) entre un symbole et une… …   Wikipédia en Français

  • Type récursif — Dans un langage de programmation, un type récursif ou type inductif est un type de données pour des valeurs qui contiennent d autres valeurs du même type. Cette notion s applique naturellement dans l étude des listes et des arbres. Sommaire 1… …   Wikipédia en Français

  • Type 90 — Char Type 90. Le char Type 90 est un char de combat japonais en service dans l’armée de terre nippone, la JGSDF (Japan Ground Self Defense Force  …   Wikipédia en Français

  • Type abstrait — En génie logiciel, un type abstrait est une spécification mathématique d un ensemble de données et de l ensemble des opérations qu elles peuvent effectuer. On qualifie d abstrait ce type de données car il correspond à un cahier des charges qu une …   Wikipédia en Français

  • Type énuméré — Pour les articles homonymes, voir Enum. En programmation informatique, un type énuméré est un type de données qui consiste en un ensemble de constantes appelées énumerateurs. Lorsque l on crée un type énuméré on définit ainsi une énumeration.… …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”