Système de types - Type system

Dans les langages de programmation , un système de types est un système logique comprenant un ensemble de règles qui attribue une propriété appelée type aux différentes constructions d'un programme informatique , telles que des variables , des expressions , des fonctions ou des modules . Ces types formalisent et appliquent les catégories par ailleurs implicites que le programmeur utilise pour les types de données algébriques , les structures de données ou d'autres composants (par exemple "chaîne", "tableau de flottants", "fonction retournant un booléen"). L'objectif principal d'un système de types est de réduire les possibilités de bogues dans les programmes informatiques en définissant des interfaces entre les différentes parties d'un programme informatique, puis en vérifiant que les parties ont été connectées de manière cohérente. Cette vérification peut se produire de manière statique (au moment de la compilation ), dynamiquement (au moment de l'exécution ) ou comme une combinaison des deux. Les systèmes de types ont également d'autres objectifs, tels que l'expression de règles métier, l'activation de certaines optimisations du compilateur , la possibilité d' envois multiples , la fourniture d'une forme de documentation, etc.

Un système de types associe un type à chaque valeur calculée et, en examinant le flux de ces valeurs, tente de garantir ou de prouver qu'aucune erreur de type ne peut se produire. Le système de types donné en question détermine ce qui constitue une erreur de type, mais en général, le but est d'empêcher les opérations qui attendent un certain type de valeur d'être utilisées avec des valeurs pour lesquelles cette opération n'a pas de sens (erreurs de validité). Les systèmes de types sont souvent spécifiés dans le cadre des langages de programmation et intégrés aux interprètes et aux compilateurs, bien que le système de types d'un langage puisse être étendu par des outils facultatifs qui effectuent des vérifications supplémentaires à l'aide de la syntaxe et de la grammaire de type d'origine du langage.

Aperçu de l'utilisation

Un exemple d'un système simple de type est celui de la langue C . Les parties d'un programme C sont les définitions de fonction . Une fonction est invoquée par une autre fonction. L'interface d'une fonction indique le nom de la fonction et une liste de paramètres qui sont passés au code de la fonction. Le code d'une fonction d'appel indique le nom de la fonction invoquée, ainsi que les noms des variables qui contiennent des valeurs à lui transmettre. Pendant l'exécution, les valeurs sont placées dans un stockage temporaire, puis l'exécution saute au code de la fonction invoquée. Le code de la fonction invoquée accède aux valeurs et les utilise. Si les instructions à l'intérieur de la fonction sont écrites avec l'hypothèse de recevoir une valeur entière , mais que le code appelant a passé une valeur à virgule flottante , alors le mauvais résultat sera calculé par la fonction invoquée. Le compilateur C vérifie les types des arguments passés à une fonction lorsqu'elle est appelée par rapport aux types des paramètres déclarés dans la définition de la fonction. Si les types ne correspondent pas, le compilateur renvoie une erreur de compilation.

Un compilateur peut également utiliser le type statique d'une valeur pour optimiser le stockage dont il a besoin et le choix des algorithmes pour les opérations sur la valeur. Dans de nombreux compilateurs C, le type de données float , par exemple, est représenté sur 32 bits , conformément à la spécification IEEE pour les nombres à virgule flottante simple précision . Ils utiliseront donc sur ces valeurs des opérations microprocesseur spécifiques à la virgule flottante (addition à virgule flottante, multiplication, etc.).

La profondeur des contraintes de type et la manière de leur évaluation affectent le typage du langage. Un langage de programmation peut en outre associer une opération avec différentes résolutions pour chaque type, dans le cas du polymorphisme de type . La théorie des types est l'étude des systèmes de types. Les types concrets de certains langages de programmation, tels que les entiers et les chaînes, dépendent de problèmes pratiques d'architecture informatique, d'implémentation de compilateur et de conception de langage.

Fondamentaux

Formellement, la théorie des types étudie les systèmes de types. Un langage de programmation doit avoir la possibilité d'effectuer une vérification de type à l'aide du système de types, que ce soit au moment de la compilation ou de l'exécution, annoté manuellement ou déduit automatiquement. Comme Mark Manasse l'a dit de façon concise :

Le problème fondamental abordé par une théorie des types est de s'assurer que les programmes ont un sens. Le problème fondamental causé par une théorie des types est que les programmes significatifs peuvent ne pas avoir de significations qui leur sont attribuées. La quête de systèmes types plus riches résulte de cette tension.

L'affectation d'un type de données, appelé typage , donne un sens à une séquence de bits telle qu'une valeur en mémoire ou un objet tel qu'une variable . Le matériel d'un ordinateur à usage général est incapable de faire la distinction entre, par exemple, une adresse mémoire et un code d'instruction , ou entre un caractère , un entier ou un nombre à virgule flottante , car il ne fait aucune distinction intrinsèque entre aucune des valeurs possibles qui une séquence de bits pourrait signifier . L'association d'une séquence de bits à un type transmet cette signification au matériel programmable pour former un système symbolique composé de ce matériel et d'un programme.

Un programme associe chaque valeur à au moins un type spécifique, mais il peut également arriver qu'une valeur soit associée à plusieurs sous-types . D'autres entités, telles que les objets , les modules , les canaux de communication et les dépendances peuvent être associées à un type. Même un type peut être associé à un type. Une implémentation d'un système de types pourrait en théorie associer des identifications appelées type de données (un type d'une valeur), classe (un type d'objet) et kind (un type d'un type ou métatype). Ce sont les abstractions par lesquelles le typage peut passer, sur une hiérarchie de niveaux contenus dans un système.

Lorsqu'un langage de programmation développe un système de types plus élaboré, il obtient un ensemble de règles plus fines que la vérification de type de base, mais cela a un prix lorsque les inférences de type (et d'autres propriétés) deviennent indécidables , et lorsqu'une plus grande attention doit être accordée par au programmeur d'annoter le code ou d'examiner les opérations et le fonctionnement liés à l'ordinateur. Il est difficile de trouver un système de types suffisamment expressif qui satisfasse toutes les pratiques de programmation d'une manière sûre pour les types .

Plus les restrictions de type imposées par le compilateur sont nombreuses, plus un langage de programmation est fortement typé . Les langages fortement typés demandent souvent au programmeur d'effectuer des conversions explicites dans des contextes où une conversion implicite ne causerait aucun dommage. Le système de types de Pascal a été décrit comme "trop ​​puissant" car, par exemple, la taille d'un tableau ou d'une chaîne fait partie de son type, ce qui rend certaines tâches de programmation difficiles. Haskell est également fortement typé mais ses types sont automatiquement déduits de sorte que les conversions explicites sont souvent inutiles.

Un compilateur de langage de programmation peut également implémenter un type dépendant ou un système d'effets , ce qui permet de vérifier encore plus de spécifications de programme par un vérificateur de type. Au-delà de simples couples valeur-type, une « région » virtuelle de code est associée à un composant « effet » décrivant ce qu'on fait avec quoi , et permettant par exemple de « lancer » un rapport d'erreur. Ainsi, le système symbolique peut être un système de types et d'effets , ce qui lui confère plus de contrôle de sécurité que le contrôle de type seul.

Qu'il soit automatisé par le compilateur ou spécifié par un programmeur, un système de types rend le comportement du programme illégal s'il est en dehors des règles du système de types. Les avantages fournis par les systèmes de type spécifiés par le programmeur incluent :

  • Abstraction (ou modularité ) – Les types permettent aux programmeurs de penser à un niveau supérieur au bit ou à l'octet, sans se soucier de l'implémentation de bas niveau. Par exemple, les programmeurs peuvent commencer à considérer une chaîne comme un ensemble de valeurs de caractères plutôt que comme un simple tableau d'octets. Plus haut encore, les types permettent aux programmeurs de penser et d'exprimer des interfaces entre deux sous-systèmes de n'importe quelle taille. Cela permet plus de niveaux de localisation afin que les définitions requises pour l'interopérabilité des sous-systèmes restent cohérentes lorsque ces deux sous-systèmes communiquent.
  • Documentation - Dans les systèmes de types plus expressifs, les types peuvent servir de forme de documentation clarifiant l'intention du programmeur. Par exemple, si un programmeur déclare une fonction comme renvoyant un type d'horodatage, cela documente la fonction lorsque le type d'horodatage peut être explicitement déclaré plus profondément dans le code pour être un type entier.

Les avantages fournis par les systèmes de types spécifiés par le compilateur incluent :

  • Optimisation – La vérification de type statique peut fournir des informations utiles au moment de la compilation. Par exemple, si un type exige qu'une valeur s'aligne en mémoire sur un multiple de quatre octets, le compilateur peut être en mesure d'utiliser des instructions machine plus efficaces.
  • Sécurité – Un système de types permet au compilateur de détecter un code sans signification ou invalide. Par exemple, nous pouvons identifier une expression 3 / "Hello, World"comme invalide, lorsque les règles ne spécifient pas comment diviser un entier par une chaîne . Une frappe forte offre plus de sécurité, mais ne peut garantir une sécurité de frappe complète .

Erreurs de saisie

Une erreur de type est une condition involontaire qui peut se manifester à plusieurs étapes du développement d'un programme. Ainsi, une facilité de détection de l'erreur est nécessaire dans le système de types. Dans certains langages, tels que Haskell, pour lesquels l' inférence de type est automatisée, lint peut être disponible pour son compilateur pour aider à la détection d'erreurs.

La sécurité de type contribue à l' exactitude du programme , mais ne peut garantir l' exactitude qu'au prix de faire de la vérification de type elle - même un problème indécidable . Dans un système de types avec vérification de type automatisée, un programme peut s'avérer ne pas fonctionner correctement sans produire d'erreurs de compilateur. La division par zéro est une opération dangereuse et incorrecte, mais un vérificateur de type exécuté uniquement au moment de la compilation ne recherche pas la division par zéro dans la plupart des langages, puis il est laissé comme une erreur d'exécution . Pour prouver l'absence de ces défauts, d'autres types de méthodes formelles , collectivement appelées analyses de programme , sont couramment utilisées. Alternativement, un système de types suffisamment expressif, comme dans les langages à typage dépendant, peut empêcher ce type d'erreurs (par exemple, exprimer le type de nombres non nuls ). De plus, les tests logiciels sont une méthode empirique pour trouver des erreurs que le vérificateur de type ne peut pas détecter.

Vérification de type

Le processus de vérification et d'application des contraintes des typesvérification de type — peut se produire au moment de la compilation (une vérification statique) ou au moment de l' exécution . Si une spécification de langage requiert fortement ses règles de typage (c'est-à-dire n'autorisant plus ou moins que les conversions de types automatiques qui ne perdent pas d'informations), on peut se référer au processus comme fortement typé , sinon, comme faiblement typé . Les termes ne sont généralement pas utilisés au sens strict.

Vérification de type statique

La vérification de type statique est le processus de vérification de la sécurité de type d'un programme basé sur l'analyse du texte d'un programme ( code source ). Si un programme réussit un vérificateur de type statique, alors le programme est assuré de satisfaire un ensemble de propriétés de sécurité de type pour toutes les entrées possibles.

La vérification de type statique peut être considérée comme une forme limitée de vérification de programme (voir sécurité de type ), et dans un langage de type sûr, peut également être considérée comme une optimisation. Si un compilateur peut prouver qu'un programme est bien typé, il n'a pas besoin d'émettre de contrôles de sécurité dynamiques, permettant au binaire compilé résultant de s'exécuter plus rapidement et d'être plus petit.

La vérification de type statique pour les langages complets de Turing est intrinsèquement conservatrice. C'est-à-dire que si un système de types est à la fois sain (c'est-à-dire qu'il rejette tous les programmes incorrects) et décidable (c'est-à-dire qu'il est possible d'écrire un algorithme qui détermine si un programme est bien typé), alors il doit être incomplet (c'est-à-dire qu'il sont des programmes corrects, qui sont également rejetés, même s'ils ne rencontrent pas d'erreurs d'exécution). Par exemple, considérons un programme contenant le code :

if <complex test> then <do something> else <signal that there is a type error>

Même si l'expression est <complex test>toujours évaluée à trueau moment de l'exécution, la plupart des vérificateurs de types rejetteront le programme comme étant mal typé, car il est difficile (voire impossible) pour un analyseur statique de déterminer que la elsebranche ne sera pas prise. Par conséquent, un vérificateur de type statique détectera rapidement les erreurs de type dans les chemins de code rarement utilisés. Sans vérification de type statique, même les tests de couverture de code avec une couverture à 100 % peuvent être incapables de trouver de telles erreurs de type. Les tests peuvent échouer à détecter de telles erreurs de type, car la combinaison de tous les endroits où les valeurs sont créées et de tous les endroits où une certaine valeur est utilisée doit être prise en compte.

Un certain nombre de fonctionnalités utiles et courantes du langage de programmation ne peuvent pas être vérifiées de manière statique, telles que le downcasting . Ainsi, de nombreux langages auront à la fois une vérification de type statique et dynamique ; le vérificateur de type statique vérifie ce qu'il peut, et les vérifications dynamiques vérifient le reste.

De nombreux langages avec vérification de type statique offrent un moyen de contourner le vérificateur de type. Certains langages permettent aux programmeurs de choisir entre la sécurité de type statique et dynamique. Par exemple, C# fait la distinction entre les variables de type statique et celles de type dynamique . Les utilisations des premiers sont vérifiées statiquement, tandis que les utilisations des seconds sont vérifiées dynamiquement. D'autres langages permettent d'écrire du code dont le type n'est pas sécurisé ; par exemple, en C , les programmeurs peuvent librement transposer une valeur entre deux types quelconques ayant la même taille, subvertissant ainsi le concept de type.

Pour obtenir la liste des langages avec vérification de type statique, consultez la catégorie des langages à typage statique .

Vérification de type dynamique et informations sur le type d'exécution

La vérification de type dynamique est le processus de vérification de la sécurité de type d'un programme au moment de l'exécution. Les implémentations de langages à vérification de type dynamique associent généralement chaque objet d'exécution à une balise de type (c'est-à-dire une référence à un type) contenant ses informations de type. Ces informations de type d'exécution (RTTI) peuvent également être utilisées pour implémenter la répartition dynamique , la liaison tardive , le downcasting , la réflexion et des fonctionnalités similaires.

La plupart des langages de type sécurisé incluent une forme de vérification de type dynamique, même s'ils disposent également d'un vérificateur de type statique. La raison en est que de nombreuses fonctionnalités ou propriétés utiles sont difficiles ou impossibles à vérifier de manière statique. Par exemple, supposons qu'un programme définisse deux types, A et B, où B est un sous-type de A. Si le programme essaie de convertir une valeur de type A en type B, ce qui est connu sous le nom de downcasting , alors l'opération n'est légale que si la valeur en cours de conversion est en fait une valeur de type B. Ainsi, une vérification dynamique est nécessaire pour vérifier que l'opération est sûre. Cette exigence est l'une des critiques du downcasting.

Par définition, la vérification de type dynamique peut entraîner l'échec d'un programme au moment de l'exécution. Dans certains langages de programmation, il est possible d'anticiper et de récupérer ces échecs. Dans d'autres, les erreurs de vérification de type sont considérées comme fatales.

Les langages de programmation qui incluent la vérification de type dynamique mais pas la vérification de type statique sont souvent appelés « langages de programmation à typage dynamique ». Pour une liste de ces langages, consultez la catégorie des langages de programmation à typage dynamique .

Combiner la vérification de type statique et dynamique

Certains langages autorisent à la fois le typage statique et dynamique. Par exemple, Java et certains autres langages à typage statique ostensible prennent en charge la conversion descendante des types vers leurs sous - types , interrogeant un objet pour découvrir son type dynamique et d'autres opérations de type qui dépendent des informations de type à l'exécution. Un autre exemple est C++ RTTI . Plus généralement, la plupart des langages de programmation incluent des mécanismes de répartition sur différents « types » de données, tels que les unions disjointes , le polymorphisme d'exécution et les types variants . Même lorsqu'ils n'interagissent pas avec les annotations de type ou la vérification de type, ces mécanismes sont matériellement similaires aux implémentations de typage dynamique. Voir langage de programmation pour plus de détails sur les interactions entre le typage statique et dynamique.

Les objets dans les langages orientés objet sont généralement accessibles par une référence dont le type cible statique (ou le type manifeste) est égal au type d'exécution de l'objet (son type latent) ou à un supertype de celui-ci. Ceci est conforme au principe de substitution de Liskov , qui stipule que toutes les opérations effectuées sur une instance d'un type donné peuvent également être effectuées sur une instance d'un sous-type. Ce concept est également connu sous le nom de subsomption ou polymorphisme de sous - type . Dans certains langages, les sous-types peuvent également posséder des types de retour covariants ou contravariants et des types d'arguments respectivement.

Certains langages, par exemple Clojure , Common Lisp ou Cython sont vérifiés de manière dynamique par défaut, mais permettent aux programmes d'opter pour la vérification de type statique en fournissant des annotations facultatives. L'une des raisons d'utiliser de telles astuces serait d'optimiser les performances des sections critiques d'un programme. Ceci est formalisé par une saisie progressive . L'environnement de programmation DrRacket , environnement pédagogique basé sur Lisp, et précurseur du langage Racket est également soft-typé.

A l'inverse, depuis la version 4.0, le langage C# permet d'indiquer qu'une variable ne doit pas être vérifiée de manière statique. Une variable dont le type est dynamicne sera pas soumise à une vérification de type statique. Au lieu de cela, le programme s'appuie sur les informations de type d'exécution pour déterminer comment la variable peut être utilisée.

Dans Rust , le type fournit un typage dynamique des types. std::any'static

Vérification de type statique et dynamique en pratique

Le choix entre le typage statique et dynamique nécessite certains compromis .

Le typage statique peut trouver des erreurs de type de manière fiable au moment de la compilation, ce qui augmente la fiabilité du programme livré. Cependant, les programmeurs ne sont pas d'accord sur la fréquence à laquelle les erreurs de type se produisent, ce qui entraîne d'autres désaccords sur la proportion de bogues codés qui seraient détectés en représentant de manière appropriée les types conçus dans le code. Les défenseurs du typage statique pensent que les programmes sont plus fiables lorsqu'ils ont été bien vérifiés, tandis que les défenseurs du typage dynamique se réfèrent au code distribué qui s'est avéré fiable et aux petites bases de données de bogues. La valeur du typage statique augmente à mesure que la force du système de typage augmente. Les partisans du typage dépendant , implémenté dans des langages tels que Dependent ML et Epigram , ont suggéré que presque tous les bogues peuvent être considérés comme des erreurs de type, si les types utilisés dans un programme sont correctement déclarés par le programmeur ou correctement déduits par le compilateur.

Le typage statique donne généralement un code compilé qui s'exécute plus rapidement. Lorsque le compilateur connaît les types de données exacts qui sont utilisés (ce qui est nécessaire pour la vérification statique, que ce soit par déclaration ou par inférence), il peut produire un code machine optimisé. Certains langages à typage dynamique tels que Common Lisp autorisent des déclarations de type facultatives pour l'optimisation pour cette raison.

En revanche, le typage dynamique peut permettre aux compilateurs de s'exécuter plus rapidement et aux interpréteurs de charger dynamiquement du nouveau code, car les modifications apportées au code source dans les langages à typage dynamique peuvent entraîner moins de vérifications à effectuer et moins de code à revisiter. Cela peut également réduire le cycle édition-compilation-test-débogage.

Les langages à typage statique qui manquent d' inférence de type (tels que C et Java avant la version 10 ) exigent que les programmeurs déclarent les types qu'une méthode ou une fonction doit utiliser. Cela peut servir de documentation de programme supplémentaire, qui est active et dynamique, au lieu d'être statique. Cela permet à un compilateur de l'empêcher de dériver de la synchronisation et d'être ignoré par les programmeurs. Cependant, un langage peut être typé statiquement sans nécessiter de déclarations de type (les exemples incluent Haskell , Scala , OCaml , F# et dans une moindre mesure C# et C++ ), donc la déclaration de type explicite n'est pas une exigence nécessaire pour le typage statique dans tous les langages.

Le typage dynamique autorise des constructions que certaines (simples) vérifications de type statique rejetteraient comme illégales. Par exemple, les fonctions eval , qui exécutent des données arbitraires sous forme de code, deviennent possibles. Une fonction eval est possible avec le typage statique, mais nécessite des utilisations avancées des types de données algébriques . En outre, le typage dynamique s'adapte mieux au code de transition et au prototypage, en permettant par exemple à une structure de données d'espace réservé ( objet fictif ) d'être utilisée de manière transparente à la place d'une structure de données complète (généralement à des fins d'expérimentation et de test).

Le typage dynamique permet généralement le typage canard (ce qui permet une réutilisation plus facile du code ). De nombreux langages avec typage statique comportent également un typage de canard ou d'autres mécanismes comme la programmation générique qui permettent également une réutilisation plus facile du code.

Le typage dynamique rend généralement la métaprogrammation plus facile à utiliser. Par exemple, les modèles C++ sont généralement plus lourds à écrire que le code Ruby ou Python équivalent car C++ a des règles plus strictes concernant les définitions de type (pour les fonctions et les variables). Cela oblige un développeur à écrire plus de code passe-partout pour un modèle qu'un développeur Python n'en aurait besoin. Les constructions d'exécution plus avancées telles que les métaclasses et l' introspection sont souvent plus difficiles à utiliser dans les langages à typage statique. Dans certains langages, de telles fonctionnalités peuvent également être utilisées, par exemple pour générer de nouveaux types et comportements à la volée, sur la base de données d'exécution. Ces constructions avancées sont souvent fournies par des langages de programmation dynamiques ; beaucoup d'entre eux sont typés dynamiquement, bien que le typage dynamique n'ait pas besoin d'être lié aux langages de programmation dynamiques .

Systèmes de type fort et faible

Les langues sont souvent appelées familièrement fortement typées ou faiblement typées . En fait, il n'y a pas de définition universellement acceptée de ce que ces termes signifient. En général, il existe des termes plus précis pour représenter les différences entre les systèmes de types qui conduisent les gens à les appeler « forts » ou « faibles ».

Sécurité de type et sécurité de la mémoire

Une troisième façon de catégoriser le système de types d'un langage de programmation est la sécurité des opérations et des conversions typées. Les informaticiens utilisent le terme langage de type sécurisé pour décrire les langages qui n'autorisent pas les opérations ou les conversions qui violent les règles du système de types.

Les informaticiens utilisent le terme langage sécurisé pour la mémoire (ou simplement langage sécurisé ) pour décrire les langages qui ne permettent pas aux programmes d'accéder à la mémoire qui n'a pas été affectée à leur utilisation. Par exemple, un langage sûr en mémoire vérifiera les limites du tableau ou garantira statiquement (c'est-à-dire au moment de la compilation avant l'exécution) que les accès au tableau en dehors des limites du tableau provoqueront des erreurs de compilation et peut-être d'exécution.

Considérez le programme suivant d'un langage à la fois sûr pour le type et pour la mémoire :

var x := 5;   
var y := "37"; 
var z := x + y;

Dans cet exemple, la variable zaura la valeur 42. Bien que ce ne soit peut-être pas ce que le programmeur avait prévu, il s'agit d'un résultat bien défini. S'il ys'agissait d'une chaîne différente, qui ne pourrait pas être convertie en nombre (par exemple, "Hello World"), le résultat serait également bien défini. Notez qu'un programme peut être de type sécurisé ou sécurisé en mémoire et quand même planter lors d'une opération invalide. C'est pour les langages où le système de types n'est pas suffisamment avancé pour spécifier avec précision la validité des opérations sur tous les opérandes possibles. Mais si un programme rencontre une opération dont le type n'est pas sécurisé, l'arrêt du programme est souvent la seule option.

Considérons maintenant un exemple similaire en C :

int x = 5;
char y[] = "37";
char* z = x + y;
printf("%c\n", *z);

Dans cet exemple , pointera vers une adresse mémoire de cinq caractères au - delà de , ce qui équivaut à trois caractères après le caractère zéro de fin de la chaîne pointée par . Il s'agit de la mémoire à laquelle le programme n'est pas censé accéder. Il peut contenir des données parasites, et il ne contient certainement rien d'utile. Comme le montre cet exemple, C n'est ni un langage sécurisé ni un langage de type sécurisé. zyy

En général, la sécurité de type et la sécurité de la mémoire vont de pair. Par exemple, un langage qui prend en charge l'arithmétique des pointeurs et les conversions nombre-à-pointeur (comme le C) n'est ni sûr en mémoire ni en type, car il permet d'accéder à une mémoire arbitraire comme s'il s'agissait d'une mémoire valide de n'importe quel type.

Pour plus d'informations, consultez la sécurité de la mémoire .

Niveaux variables de vérification de type

Certaines langues permettent à différents niveaux de vérification de s'appliquer à différentes régions de code. Les exemples comprennent:

  • La use strictdirective en JavaScript et Perl applique une vérification plus stricte.
  • Le declare(strict_types=1)en PHP sur une base par fichier permet seulement une variable de type exact de la déclaration de type sera acceptée, ou un TypeErrorsera lancé.
  • Le Option Strict Ondans VB.NET permet au compilateur d'exiger une conversion entre les objets.

Des outils supplémentaires tels que lint et IBM Rational Purify peuvent également être utilisés pour atteindre un niveau de rigueur plus élevé.

Systèmes de types en option

Il a été proposé, principalement par Gilad Bracha , que le choix du système de types soit indépendant du choix de la langue ; qu'un système de types doit être un module qui peut être connecté à une langue selon les besoins. Il pense que c'est avantageux, car ce qu'il appelle les systèmes de types obligatoires rendent les langages moins expressifs et le code plus fragile. L'exigence selon laquelle le système de types n'affecte pas la sémantique du langage est difficile à satisfaire.

La saisie facultative est liée à la saisie graduelle , mais distincte de celle-ci . Bien que les deux disciplines de typage puissent être utilisées pour effectuer une analyse statique du code ( typage statique ), les systèmes de types facultatifs n'appliquent pas la sécurité des types au moment de l'exécution ( typage dynamique ).

Polymorphisme et types

Le terme polymorphisme fait référence à la capacité du code (en particulier, des fonctions ou des classes) à agir sur des valeurs de types multiples, ou à la capacité de différentes instances de la même structure de données à contenir des éléments de types différents. Les systèmes de types qui permettent le polymorphisme le font généralement afin d'améliorer le potentiel de réutilisation du code : dans un langage avec polymorphisme, les programmeurs n'ont besoin d'implémenter une structure de données telle qu'une liste ou un tableau associatif qu'une seule fois, plutôt qu'une fois pour chaque type de élément avec lequel ils prévoient de l'utiliser. Pour cette raison, les informaticiens appellent parfois l'utilisation de certaines formes de polymorphisme la programmation générique . Les fondements de la théorie des types du polymorphisme sont étroitement liés à ceux de l' abstraction , de la modularité et (dans certains cas) du sous-typage .

Systèmes de types spécialisés

De nombreux systèmes de types ont été créés et sont spécialisés pour une utilisation dans certains environnements avec certains types de données, ou pour l' analyse de programme statique hors bande . Fréquemment, ceux-ci sont basés sur des idées de la théorie formelle des types et ne sont disponibles que dans le cadre de systèmes de recherche prototypes.

Le tableau suivant donne un aperçu des concepts théoriques des types utilisés dans les systèmes de types spécialisés. Les noms M, N, O s'étendent sur les termes et les noms sur les types. La notation (resp. ) décrit le type qui résulte du remplacement de toutes les occurrences du type variable α (resp. terme variable x ) dans τ par le type σ (resp. terme N ).

Notion de type Notation Sens
Fonction Si M est de type et N de type σ , alors l'application est de type τ .
Produit Si M est de type , puis est une paire de telle sorte que N a le type σ et O a de type τ .
Somme Si M est de type , alors soit est la première injection de telle sorte que N est de type σ , ou

est la deuxième injection de telle sorte que N est de type τ .

Intersection Si M est de type , alors M est de type σ et M de type τ .
syndicat Si M est de type , alors M est de type σ ou M est de type τ .
Enregistrer Si M est de type , alors M a un élément x qui a le type τ .
Polymorphe Si M est de type , alors M est de type pour tout type σ .
Existentiel Si M a le type , alors M a le type pour un certain type σ .
Récursif Si M a le type , alors M a le type .
Fonction dépendante Si M est de type et N de type σ , alors l'application est de type .
Produit dépendant Si M est de type , puis est une paire de telle sorte que N a le type σ et O a le type .
Intersection dépendante Si M est de type , alors M de type σ et M de type .
Carrefour familial Si M est de type , alors M est de type pour tout terme N de type σ .
Union familiale Si M est de type , alors M est de type pour un terme N de type σ .

Types dépendants

Les types dépendants sont basés sur l'idée d'utiliser des scalaires ou des valeurs pour décrire plus précisément le type d'une autre valeur. Par exemple, peut être le type d'une matrice. On peut alors définir des règles de typage telles que la règle suivante pour la multiplication matricielle :

k , m , n sont des valeurs entières positives arbitraires. Une variante de ML appelée Dependent ML a été créée sur la base de ce système de types, mais comme la vérification de type pour les types dépendants conventionnels est indécidable , tous les programmes qui les utilisent ne peuvent pas être vérifiés sans aucune sorte de limites. Le ML dépendant limite le type d'égalité qu'il peut décider à l'arithmétique de Presburger .

D'autres langages tels que Epigram rendent la valeur de toutes les expressions dans le langage décidable afin que la vérification de type puisse être décidable. Cependant, en général, la preuve de décidabilité est indécidable , donc de nombreux programmes nécessitent des annotations manuscrites qui peuvent être très peu triviales. Comme cela entrave le processus de développement, de nombreuses implémentations de langage offrent une solution de facilité sous la forme d'une option pour désactiver cette condition. Ceci, cependant, a le prix de faire fonctionner le vérificateur de type dans une boucle infinie lorsqu'il est alimenté par des programmes qui ne vérifient pas le type, provoquant l'échec de la compilation.

Types linéaires

Les types linéaires , basés sur la théorie de la logique linéaire , et étroitement liés aux types d'unicité , sont des types affectés à des valeurs ayant la propriété d'avoir une et une seule référence à tout moment. Ceux-ci sont précieux pour décrire de grandes valeurs immuables telles que des fichiers, des chaînes, etc., car toute opération qui détruit simultanément un objet linéaire et crée un objet similaire (tel que ' str= str + "a"') peut être optimisée "sous le capot" dans un mutation de lieu. Normalement, cela n'est pas possible, car de telles mutations pourraient provoquer des effets secondaires sur des parties du programme contenant d'autres références à l'objet, violant ainsi la transparence référentielle . Ils sont également utilisés dans le prototype de système d'exploitation Singularity pour la communication interprocessus, garantissant statiquement que les processus ne peuvent pas partager des objets dans la mémoire partagée afin d'éviter les conditions de concurrence. Le langage Clean (un langage semblable à Haskell ) utilise ce système de types afin de gagner beaucoup de vitesse (par rapport à une copie en profondeur) tout en restant en sécurité.

Types d'intersections

Intersection types sont des types qui décrivent les valeurs qui appartiennent à la fois de deux autres types donnés avec des ensembles de valeurs qui se chevauchent. Par exemple, dans la plupart des implémentations de C, le caractère signé a une plage de -128 à 127 et le caractère non signé a une plage de 0 à 255, donc le type d'intersection de ces deux types aurait une plage de 0 à 127. Un tel type d'intersection pourrait être passé en toute sécurité. en fonctions attendent soit les caractères non signés ou signés, car il est compatible avec les deux types.

Les types d'intersection sont utiles pour décrire les types de fonction surchargés : par exemple, si " → " est le type de fonctions prenant un argument entier et retournant un entier, et " → " est le type de fonctions prenant un argument flottant et retournant un flottant, alors l'intersection de ces deux types peut être utilisée pour décrire des fonctions qui font l'un ou l'autre, en fonction du type d'entrée qui leur est fournie. Une telle fonction pourrait être passée à une autre fonction en attendant une fonction " → " en toute sécurité ; il n'utiliserait tout simplement pas la fonctionnalité " → ". intintfloatfloatintintfloatfloat

Dans une hiérarchie de sous-classes, l'intersection d'un type et d'un type ancêtre (comme son parent) est le type le plus dérivé. L'intersection des types frères est vide.

Le langage Forsythe inclut une implémentation générale des types d'intersection. Une forme restreinte est les types de raffinement .

Types de syndicats

Les types d'union sont des types décrivant des valeurs qui appartiennent à l' un des deux types. Par exemple, en C, le caractère signé a une plage de -128 à 127, et le caractère non signé a une plage de 0 à 255, donc l'union de ces deux types aurait une plage "virtuelle" globale de -128 à 255 qui peut être utilisé partiellement en fonction du membre du syndicat auquel on accède. Toute fonction gérant ce type d'union devrait traiter des entiers dans cette plage complète. Plus généralement, les seules opérations valides sur un type d'union sont les opérations valides sur les deux types en cours d'union. Le concept "union" de C est similaire aux types union, mais n'est pas sécurisé, car il permet des opérations valides sur l'un ou l'autre type, plutôt que sur les deux . Les types d'union sont importants dans l'analyse de programme, où ils sont utilisés pour représenter des valeurs symboliques dont la nature exacte (par exemple, la valeur ou le type) n'est pas connue.

Dans une hiérarchie de sous-classes, l'union d'un type et d'un type ancêtre (comme son parent) est le type ancêtre. L'union des types frères est un sous-type de leur ancêtre commun (c'est-à-dire que toutes les opérations autorisées sur leur ancêtre commun sont autorisées sur le type union, mais ils peuvent également avoir d'autres opérations valides en commun).

Types existentiels

Les types existentiels sont fréquemment utilisés en relation avec les types d'enregistrement pour représenter des modules et des types de données abstraits , en raison de leur capacité à séparer l'implémentation de l'interface. Par exemple, le type "T = ∃X { a: X; f: (X → int); }" décrit une interface de module qui a une donnée membre nommée a de type X et une fonction nommée f qui prend un paramètre de la même type X et renvoie un entier. Cela pourrait être mis en œuvre de différentes manières; par exemple:

  • intT = { a: int; f : (entier → entier) ; }
  • floatT = { a: float; f : (float → entier) ; }

Ces types sont tous deux des sous-types du type existentiel plus général T et correspondent à des types d'implémentation concrets, donc toute valeur de l'un de ces types est une valeur de type T. Étant donné une valeur "t" de type "T", nous savons que " tf (ta) » est bien typé, quel que soit le type abstrait X est. Cela donne une flexibilité pour choisir les types adaptés à une implémentation particulière tandis que les clients qui n'utilisent que des valeurs du type d'interface (le type existentiel) sont isolés de ces choix.

En général, il est impossible pour le vérificateur de types de déduire à quel type existentiel un module donné appartient. Dans l'exemple ci-dessus intT { a: int; f : (entier → entier) ; } pourrait aussi avoir le type ∃X { a: X; f : (entier → entier) ; }. La solution la plus simple consiste à annoter chaque module avec son type prévu, par exemple :

  • intT = { a: int; f : (entier → entier) ; } comme ∃X { a: X; f : (X → entier) ; }

Bien que les types de données abstraits et les modules aient été implémentés dans les langages de programmation depuis un certain temps, ce n'est qu'en 1988 que John C. Mitchell et Gordon Plotkin ont établi la théorie formelle sous le slogan : « Les types abstraits [de données] ont un type existentiel ». La théorie est un calcul lambda typé du second ordre similaire au système F , mais avec une quantification existentielle au lieu d'une quantification universelle.

Saisie progressive

Le typage graduel est un système de types dans lequel les variables peuvent se voir attribuer un type soit au moment de la compilation (qui est un typage statique) soit à l' exécution (qui est un typage dynamique), permettant aux développeurs de logiciels de choisir l'un ou l'autre type de paradigme, le cas échéant, depuis l'intérieur une seule langue. En particulier, le typage graduel utilise un type spécial nommé dynamic pour représenter les types statiquement inconnus, et le typage graduel remplace la notion d'égalité de type par une nouvelle relation appelée cohérence qui relie le type dynamique à tous les autres types. La relation de cohérence est symétrique mais non transitive.

Déclaration et inférence explicites ou implicites

De nombreux systèmes de types statiques, tels que ceux de C et Java, nécessitent des déclarations de type : le programmeur doit associer explicitement chaque variable à un type spécifique. D'autres, comme Haskell, effectuent une inférence de type : le compilateur tire des conclusions sur les types de variables en fonction de la façon dont les programmeurs utilisent ces variables. Par exemple, étant donné une fonction qui ajoute et ensemble, le compilateur peut déduire que et doit être des nombres, puisque l'addition n'est définie que pour les nombres. Ainsi, tout appel ailleurs dans le programme qui spécifie un type non numérique (comme une chaîne ou une liste) comme argument signalerait une erreur. f(x, y)xyxyf

Les constantes et expressions numériques et de chaîne dans le code peuvent impliquer et impliquent souvent un type dans un contexte particulier. Par exemple, une expression 3.14peut impliquer un type de virgule flottante , tandis qu'elle peut impliquer une liste d'entiers, généralement un tableau . [1, 2, 3]

L'inférence de types est en général possible, si elle est calculable dans le système de types en question. De plus, même si l'inférence n'est pas calculable en général pour un système de types donné, l'inférence est souvent possible pour un grand sous-ensemble de programmes du monde réel. Le système de types de Haskell, une version de Hindley-Milner , est une restriction du système Fω aux types polymorphes dits de rang 1, dans lesquels l'inférence de types est calculable. La plupart des compilateurs Haskell autorisent le polymorphisme de rang arbitraire comme extension, mais cela rend l'inférence de type non calculable. ( Cependant, la vérification de type est décidable et les programmes de rang 1 ont toujours une inférence de type ; les programmes polymorphes de rang supérieur sont rejetés à moins qu'ils ne reçoivent des annotations de type explicites.)

Problèmes de décision

Un système de types qui assigne des types à des termes dans des environnements de types à l'aide de règles de types est naturellement associé aux problèmes de décision de vérification de type , de typabilité et d' habitation de type .

  • Étant donné un environnement de type , un terme et un type , décidez si le terme peut se voir attribuer le type dans l'environnement de type.
  • Étant donné un terme , décidez s'il existe un environnement de type et un type tels que le terme puisse se voir attribuer le type dans l'environnement de type .
  • Étant donné un environnement de type et un type , décidez s'il existe un terme auquel le type peut être affecté dans l'environnement de type.

Système de type unifié

Certains langages comme C# ou Scala ont un système de type unifié. Cela signifie que tous les types C#, y compris les types primitifs, héritent d'un seul objet racine. Chaque type en C# hérite de la classe Object. Certains langages, comme Java et Raku , ont un type racine mais aussi des types primitifs qui ne sont pas des objets. Java fournit des types d'objet wrapper qui existent avec les types primitifs afin que les développeurs puissent utiliser les types d'objet wrapper ou les types primitifs non-objet plus simples. Raku convertit automatiquement les types primitifs en objets lorsque leurs méthodes sont accessibles.

Compatibilité : équivalence et sous-typage

Un vérificateur de type pour un langage à typage statique doit vérifier que le type de toute expression est cohérent avec le type attendu par le contexte dans lequel cette expression apparaît. Par exemple, dans une instruction d'affectation de la forme , le type inféré de l'expression doit être cohérent avec le type déclaré ou inféré de la variable . Cette notion de cohérence, appelée compatibilité , est propre à chaque langage de programmation. x := eex

Si le type de eet le type de xsont identiques et que l'affectation est autorisée pour ce type, il s'agit d'une expression valide. Ainsi, dans les systèmes de types les plus simples, la question de savoir si deux types sont compatibles se réduit à celle de savoir s'ils sont égaux (ou équivalents ). Différentes langues, cependant, ont des critères différents pour le moment où deux expressions de type sont comprises comme dénotant le même type. Ces différentes théories équationnelles des types varient considérablement, deux cas extrêmes étant les systèmes de types structurels , dans lesquels deux types quelconques qui décrivent des valeurs avec la même structure sont équivalents, et les systèmes de types nominatifs , dans lesquels deux expressions de types syntaxiquement distinctes ne désignent pas le même type ( c'est-à - dire que les types doivent avoir le même "nom" pour être égaux).

Dans les langages avec sous - typage , la relation de compatibilité est plus complexe. En particulier, si Best un sous-type de A, alors une valeur de type Bpeut être utilisée dans un contexte où une valeur de type Aest attendue ( covariant ), même si l'inverse n'est pas vrai. Comme l'équivalence, la relation de sous-type est définie différemment pour chaque langage de programmation, avec de nombreuses variantes possibles. La présence de polymorphisme paramétrique ou ad hoc dans un langage peut également avoir des implications pour la compatibilité de type.

Voir également

Remarques

Les références

Lectures complémentaires

Liens externes