Worldlex Wiki Un système de types simple pour un langage de programmation est un ensemble de règles qui associe un type de données (par exemple, entier , nombre à virgule flottante , chaîne de caractères ) à chaque terme (expression à valeurs de données) d'un programme informatique . Dans des systèmes de types plus ambitieux, diverses constructions, telles que les variables , les expressions , les fonctions et les modules , peuvent se voir attribuer des types.
Les systèmes de types formalisent et appliquent les catégories autrement implicites que le programmeur utilise pour les types de données algébriques , les structures de données ou d'autres types de données , tels que « chaîne de caractères », « tableau de nombres flottants », « fonction renvoyant un booléen ».
L'objectif principal d'un système de types dans un langage de programmation est de réduire les risques d' erreurs dans les programmes informatiques dues à des incohérences d'interprétation des valeurs dans différentes parties du programme. Il s'agit d'empêcher l'application d'opérations attendant un certain type de valeur à des valeurs pour lesquelles cette opération n'a pas de sens (erreurs de validité). Un système de types peut détecter et prévenir certaines de ces incohérences. Lorsqu'une incohérence de type est détectée, on parle d' erreur de type .
Le type d'un terme restreint les contextes dans lesquels il peut être utilisé. Pour une variable, le système de types détermine les valeurs autorisées. Pour qu'une variable puisse être passée comme paramètre à une opération, cette dernière doit pouvoir accepter, dans ce paramètre, toute valeur autorisée par le type de la variable.
Les systèmes de types sont généralement spécifiés lors de la conception des langages de programmation . Ils sont intégrés aux interpréteurs et aux compilateurs du langage. Dans certains langages, le système de types peut être étendu par des outils optionnels qui effectuent des vérifications supplémentaires en utilisant la syntaxe et la grammaire de types d'origine du langage .
Les systèmes de types permettent de définir des interfaces entre les différentes parties d'un programme informatique, puis de vérifier que ces parties sont connectées de manière cohérente. Cette vérification peut être statique (à la compilation ), dynamique (à l'exécution ) ou une combinaison des deux.
Les systèmes de types ont également d'autres objectifs, tels que l'expression de règles métier, la possibilité de certaines optimisations du compilateur , la possibilité de répartitions multiples et la fourniture d'une forme de documentation .
langage C est un exemple de système de types simple . Les parties d'un programme C sont les définitions de fonctions . Une fonction est appelée par une autre.L' interface d'une fonction indique son nom et la liste des paramètres qui lui sont transmis. Le code de la fonction appelante indique son nom, ainsi que les noms des variables qui contiennent les valeurs à lui transmettre.
Lors de l'exécution d'un programme informatique , les valeurs sont stockées temporairement, puis l'exécution se poursuit avec le code de la fonction appelée. Ce code accède alors aux valeurs et les utilise.
Si les instructions à l'intérieur de la fonction sont écrites en supposant la réception d'une valeur entière , mais que le code appelant a passé une valeur à virgule flottante , alors le résultat calculé par la fonction invoquée sera incorrect.
Le compilateur C vérifie la concordance des types des arguments passés à une fonction lors de son appel avec les types des paramètres déclarés dans sa définition. En cas de non-concordance, le compilateur génère une erreur ou un avertissement à la compilation.
Un compilateur peut également utiliser le type statique d'une valeur pour optimiser l'espace de stockage nécessaire et le choix des algorithmes pour les opérations sur cette 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 des opérations spécifiques aux microprocesseurs pour les nombres à virgule flottante (addition, multiplication, etc.).
La profondeur des contraintes de type et leur mode d'évaluation influent sur le typage du langage. Un langage de programmation peut, en outre, associer une opération à différentes résolutions pour chaque type, dans le cas du polymorphisme de types . 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 de caractères, dépendent de contraintes pratiques liées à l'architecture des ordinateurs , à l'implémentation du compilateur et à la conception du langage .
Principes 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 à la compilation ou à l'exécution, par annotation manuelle ou par inférence automatique. Comme l'a formulé Mark Manasse de manière concise :
Le problème fondamental auquel s'attaque une théorie des types est de garantir que les programmes aient une signification. Le problème fondamental engendré par une théorie des types est que des programmes ayant une signification peuvent ne pas se voir attribuer de signification. La recherche de systèmes de types plus riches découle de cette tension.
L'attribution d'un type de données, appelée typage , confère une signification à une séquence de bits , comme une valeur en mémoire ou un objet tel qu'une variable . Le matériel d'un ordinateur généraliste est incapable de distinguer, par exemple, une adresse mémoire d'un code d'instruction , ou un caractère , un entier ou un nombre à virgule flottante , car il ne fait aucune distinction intrinsèque entre les différentes valeurs possibles qu'une séquence de bits peut représenter . L'association d'une séquence de bits à un type transmet cette signification au matériel programmable afin de 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 une même valeur peut être associée à plusieurs sous-types . D'autres entités, telles que des objets , des modules , des canaux de communication et des dépendances , peuvent être associées à un type. Un type peut même être associé à un autre type. En théorie, l'implémentation d'un système de types pourrait associer des identifications appelées type de données (le type d'une valeur), classe (le type d'un objet) et genre (le type d'un type , ou métatype). Ce sont les abstractions que le typage peut appliquer, selon une hiérarchie de niveaux au sein du système.
Lorsqu'un langage de programmation développe un système de types plus élaboré, il acquiert un ensemble de règles plus précis que la vérification de types de base. Cependant, cette finesse a un coût : les inférences de types (et autres propriétés) deviennent indécidables , et le programmeur doit accorder une attention accrue à l'annotation du code et à la prise en compte des opérations et du fonctionnement de l'ordinateur. Trouver un système de types suffisamment expressif qui garantisse la sécurité des types tout en respectant toutes les pratiques de programmation représente un véritable défi .
Un compilateur de langage de programmation peut également implémenter un système de types dépendants ou un système d'effets , permettant ainsi à un vérificateur de types de contrôler un plus grand nombre de spécifications de programme. Au-delà des simples paires valeur-type, une « région » virtuelle de code est associée à un composant « d'effet » décrivant les opérations effectuées sur les données et permettant, par exemple, de générer un rapport d'erreur. Le système symbolique peut donc être un système de types et d'effets , ce qui lui confère un niveau de sécurité supérieur à celui du seul contrôle de types.
Qu’il soit automatisé par le compilateur ou défini par le programmeur, un système de types rend illégal tout comportement de programme qui ne respecte pas ses règles. Les avantages des systèmes de types définis par le programmeur sont les suivants :
- Abstraction (ou modularité ) – Les types permettent aux programmeurs de raisonner à un niveau supérieur, au-delà du bit ou de l'octet, sans se soucier de l'implémentation de bas niveau . Par exemple, ils peuvent considérer une chaîne de caractères comme un ensemble de valeurs de caractères plutôt que comme un tableau d'octets. Plus précisément, les types permettent de concevoir et d'exprimer des interfaces entre deux sous-systèmes de taille quelconque . Ceci permet une localisation plus poussée, garantissant ainsi la cohérence des définitions nécessaires à l'interopérabilité des sous-systèmes lors de leurs communications.
- Documentation – Dans les systèmes de types plus expressifs, les types peuvent servir de documentation, clarifiant ainsi l'intention du programmeur. Par exemple, si un programmeur déclare une fonction comme renvoyant un type timestamp, cela documente la fonction alors que le type timestamp peut être explicitement déclaré plus loin dans le code comme étant un type entier.
Les avantages offerts par les systèmes de types spécifiés par le compilateur comprennent :
- Optimisation – La vérification statique des types peut fournir des informations utiles lors de la compilation . Par exemple, si un type exige qu'une valeur soit alignée en mémoire sur un multiple de quatre octets, le compilateur pourra utiliser des instructions machine plus efficaces.
- Sécurité – Un système de types permet au compilateur de détecter le code invalide ou incohérent. Par exemple, une expression peut être identifiée comme invalide si les règles ne précisent pas comment diviser un entier par une chaîne de caractères . Un typage fort offre une sécurité accrue, mais ne garantit pas une sécurité de type absolue .
3 / "Hello, World"
Erreurs de frappe
Une erreur de type se produit lorsqu'une opération reçoit des données d'un type différent de celui attendu. Par exemple, une erreur de type survient si une ligne de code effectuant une division entre deux entiers reçoit une chaîne de caractères au lieu d'un entier. Il s'agit d'une situation imprévue susceptible de se manifester à différentes étapes du développement d'un programme. Un mécanisme de détection de cette erreur est donc nécessaire au sein du système de types. Dans certains langages, comme Haskell , où l'inférence de types est automatisée, un outil d'analyse statique de code (lint) peut être mis à la disposition du compilateur pour faciliter la détection de cette erreur.
La sûreté des types contribue à la correction des programmes , mais peut ne la garantir qu'au prix de rendre la vérification des types elle-même indécidable (comme dans le problème de l'arrêt ). Dans un système de types avec vérification automatique, un programme peut s'exécuter incorrectement sans pour autant générer d'erreurs de compilation. La division par zéro est une opération dangereuse et incorrecte, mais un vérificateur de types exécuté uniquement à la compilation ne recherche généralement pas les divisions par zéro ; cette division se manifesterait alors par une erreur d'exécution . Pour prouver l'absence de ces défauts, d'autres méthodes formelles , appelées analyses de programmes , sont couramment utilisées. Par ailleurs, un système de types suffisamment expressif, comme dans les langages à types dépendants, peut prévenir ces erreurs (par exemple, en précisant le type des nombres non nuls ). Enfin, les tests logiciels constituent une méthode empirique pour identifier les erreurs qu'un tel vérificateur de types ne détecterait pas.
Vérification de type
Le processus de vérification et d'application des contraintes de types, appelé vérification de type , peut avoir lieu au moment de la compilation (vérification statique) ou au moment de l'exécution (vérification dynamique).
Si une spécification de langage exige que ses règles de typage soient strictes, n'autorisant plus ou moins que les conversions de type automatiques qui ne perdent pas d'information, on peut qualifier le processus de fortement typé ; sinon, de faiblement typé .
Ces termes ne sont généralement pas utilisés au sens strict.
Vérification statique des types
La vérification statique des types peut être considérée comme une forme limitée de vérification de programme (voir sécurité des types ) et, dans un langage à typage statique, comme une optimisation. Si un compilateur peut prouver qu'un programme est bien typé, il n'a pas besoin d'effectuer de vérifications de sécurité dynamiques, ce qui permet d'obtenir un binaire compilé plus rapide et plus compact.
La vérification statique des types pour les langages Turing-complets est intrinsèquement conservatrice. Autrement dit, si un système de types est à la fois correct (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 est nécessairement incomplet (c'est-à-dire qu'il existe 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 suivant :
if <complex test> then <do something> else <signal that there is a type error>
Même si l'expression <complex test>est toujours évaluée à vrai trueà 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 empruntée. Par conséquent, un vérificateur de types statique détectera rapidement les erreurs de type dans les chemins d'exécution rarement utilisés. Sans vérification statique des types, même des tests de couverture de code à 100 % peuvent ne pas détecter de telles erreurs. Ces tests peuvent échouer car il est nécessaire de prendre en compte l'ensemble des occurrences de création et d'utilisation des valeurs.
De nombreuses fonctionnalités utiles et courantes des langages de programmation ne peuvent être vérifiées statiquement, comme la conversion descendante de type . C'est pourquoi de nombreux langages combinent vérification statique et dynamique des types : le vérificateur statique vérifie ce qu'il peut, et les vérifications dynamiques le reste.
De nombreux langages à typage statique offrent la possibilité de contourner le vérificateur de types. Certains langages permettent aux programmeurs de choisir entre la sécurité statique et dynamique des types. Par exemple, historiquement, C# déclare les variables de manière statique , mais C# 4.0 introduit le dynamicmot-clé `static`, utilisé pour déclarer des variables à vérifier dynamiquement à l’exécution D’autres langages permettent d’écrire du code non sécurisé au niveau des types ; par exemple, en C , les programmeurs peuvent convertir librement une valeur entre deux types quelconques de même taille, ce qui revient à contourner le concept de typage.
Vérification dynamique des types et informations de type à l'exécution
La plupart des langages à typage statique incluent une forme de vérification dynamique des types, même s'ils disposent également d'un vérificateur statique. En effet, de nombreuses fonctionnalités ou propriétés utiles sont difficiles, voire impossibles, à vérifier statiquement. Par exemple, supposons qu'un programme définisse deux types, A et B, où B est un sous-type de A. Si le programme tente de convertir une valeur de type A en type B (opération appelée conversion descendante ), cette conversion n'est valide que si la valeur convertie est effectivement de type B. Une vérification dynamique est donc nécessaire pour garantir la sécurité de l'opération. Cette exigence constitue l'une des critiques formulées à l'encontre de la conversion descendante.
Par définition, la vérification dynamique des types peut entraîner l'échec d'un programme à l'exécution. Dans certains langages de programmation, il est possible d'anticiper et de corriger ces échecs. Dans d'autres, les erreurs de vérification des types sont considérées comme fatales.
Les langages de programmation qui incluent une vérification dynamique des types mais pas une vérification statique des types sont souvent appelés « langages de programmation à typage dynamique ».
Combinaison de la vérification statique et dynamique des types
Certains langages, comme Clojure , Common Lisp ou Cython, sont par défaut soumis à un typage dynamique, mais permettent d'activer le typage statique via des annotations optionnelles. L'utilisation de ces annotations permet notamment d'optimiser les performances des sections critiques d'un programme. Ce principe est formalisé par le typage progressif . L'environnement de programmation DrRacket , un environnement pédagogique basé sur Lisp et précurseur du langage Racket, est également à typage souple.
À l'inverse, depuis la version 4.0, le langage C# offre la possibilité d'indiquer qu'une variable ne doit pas faire l'objet d'une vérification statique de type. Une variable de type `None` dynamicne sera pas soumise à cette vérification. Le programme s'appuiera alors sur les informations de type obtenues à l'exécution pour déterminer comment la variable peut être utilisée.
En Rust , l' objet trait fournit un typage dynamique des types ne contenant aucune ou seulement des durées de vie. compromis .
Le typage statique permet de détecter les erreurs de type de manière fiable à la compilation, ce qui accroît la fiabilité du programme livré. Cependant, les programmeurs divergent quant à la fréquence d'apparition des erreurs de type, ce qui engendre des désaccords supplémentaires sur la proportion de bogues qui seraient détectés par une représentation adéquate des types conçus dans le code. Les partisans du typage statique estiment que les programmes sont plus fiables lorsqu'ils ont fait l'objet d'une vérification de type rigoureuse, tandis que les partisans du typage dynamique mettent en avant le code distribué, dont la fiabilité est avérée, et la taille réduite des bases de données de bogues. L'intérêt du typage statique augmente avec la robustesse du système de types. Les partisans du typage dépendant , implémenté dans des langages tels que Dependent ML et Epigram , suggèrent que la quasi-totalité des 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 inférés par le compilateur.
Le typage statique permet généralement d'obtenir un code compilé plus rapide à l'exécution. Lorsque le compilateur connaît les types de données exacts utilisés (ce qui est nécessaire pour la vérification statique, par déclaration ou inférence), il peut générer un code machine optimisé. C'est pourquoi certains langages à typage dynamique, comme Common Lisp, autorisent les déclarations de types optionnelles à des fins d'optimisation.
À l'inverse, 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 à réexaminer. d'inférence de types (comme C et Java avant la version 10 ) exigent que les programmeurs déclarent les types utilisés par une méthode ou une fonction. Ceci constitue une documentation supplémentaire, active et dynamique, contrairement à la documentation statique. Le compilateur peut ainsi éviter toute désynchronisation et empêcher que cette documentation ne soit ignorée par les programmeurs. Cependant, un langage peut être statiquement typé sans exiger de déclarations de types (par exemple, Haskell , Scala , OCaml , F# , Swift et, dans une moindre mesure , C# et C++ ). Par conséquent, la déclaration explicite des types n'est pas requise pour le typage statique dans tous les langages.
Le typage dynamique autorise des constructions que certains typages statiques (simples) rejetteraient comme illégales. Par exemple, les fonctions `eval` , qui exécutent des données arbitraires comme du code, deviennent possibles. Une fonction `eval` est possible avec le typage statique, mais nécessite une utilisation avancée des types de données algébriques . De plus, le typage dynamique s'adapte mieux au code transitoire et au prototypage, permettant par exemple d'utiliser de manière transparente une structure de données factice ( objet factice ) à 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 (qui facilite la réutilisation du code ). De nombreux le typage canard ou d'autres mécanismes comme la programmation générique, qui facilitent également la réutilisation du code.
Le typage dynamique facilite généralement l'utilisation de la métaprogrammation . Par exemple, les modèles C++ sont généralement plus complexes à écrire que le code équivalent en Ruby ou Python , car le C++ impose des règles plus strictes concernant les définitions de types (pour les fonctions comme pour les variables). Cela oblige un développeur à écrire davantage de code répétitif pour un modèle qu'un développeur Python. Les constructions d'exécution plus avancées, telles que les métaclasses et l'introspection, sont souvent plus difficiles à utiliser dans les langages statiquement typés. Dans certains langages, ces fonctionnalités peuvent également servir, par exemple, à générer dynamiquement de nouveaux types et comportements à partir des données d'exécution. Ces constructions avancées sont souvent fournies par les langages de programmation dynamique ; nombre d'entre eux sont à typage dynamique, bien que le typage dynamique ne soit pas nécessairement lié aux langages de programmation dynamique .
systèmes de types forts et faibles
Considérons le programme suivant d'un langage à la fois sûr en termes de types et sûr en termes de mémoire :
Dans cet exemple, la variable Hello, World »), le résultat serait également conforme aux attentes. Un programme peut être sûr du point de vue des types et de la gestion de la mémoire et pourtant planter lors d'une opération invalide. Cela concerne les langages dont le système de types n'est pas suffisamment avancé pour spécifier précisément la validité des opérations sur tous les opérandes possibles. Mais si un programme rencontre une opération non sûre du point de vue des types, l'arrêt du programme est souvent la seule solution.
Considérons maintenant un exemple similaire en C :
Dans cet exemple, ` comportement est indéfini et le programme peut effectuer n'importe quelle action ; avec un compilateur simple, il pourrait même afficher l'octet stocké après la chaîne « 37 ». Comme le montre cet exemple, le C n'est pas sûr en matière de gestion de la mémoire. De plus, comme des données arbitraires ont été considérées comme des caractères, le C n'est pas non plus un langage à typage statique.
En général, la sécurité des types et la sécurité de la mémoire sont indissociables. Par exemple, un langage qui prend en charge l'arithmétique des pointeurs et les conversions de nombres en pointeurs (comme le C) n'est ni sûr en termes de mémoire ni en termes de types, car il permet d'accéder à une zone mémoire arbitraire comme s'il s'agissait d'une zone mémoire valide de n'importe quel type.
Niveaux variables de vérification de type
Certains langages permettent d'appliquer différents niveaux de vérification à différentes régions du code. En voici quelques exemples :
- La
use strictdirective en JavaScript et Perl applique une vérification plus forte. - Le
declare(strict_types=1)PHP sur une base de fichier permet uniquement une variable du type exact de la déclaration de type sera acceptée, ou une exception sera levée.TypeError - En VB.NET,
Option Strict Oncela 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 type optionnel
Il a été proposé, principalement par Gilad Bracha , que le choix du système de types soit indépendant du choix du langage ; qu’un système de types soit un module pouvant être intégré au langage selon les besoins. Il estime que cela présente un avantage, 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.
Le typage optionnel est lié au typage progressif , mais s'en distingue . 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 optionnels n'imposent pas la sécurité des types à l'exécution ( typage dynamique ).
Polymorphisme et types
Systèmes de types spécialisés
De nombreux systèmes de types ont été créés, spécialisés pour une utilisation dans certains environnements avec certains types de données, ou pour l'analyse statique de programmes hors bande . Souvent, ils reposent sur des concepts 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 de la théorie des types utilisés dans les systèmes de types spécialisés. Les noms
Types linéaires
str = str + "a") peut être optimisée en interne en une mutation sur place. Normalement, cela est impossible, car de telles mutations pourraient engendrer des effets de bord sur les 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 système d'exploitation prototype Singularity pour la communication interprocessus, garantissant statiquement que les processus ne peuvent pas partager d'objets en mémoire partagée afin d'éviter les conditions de concurrence. Le langage Clean (un langage de type Haskell ) utilise ce système de types pour gagner considérablement en vitesse (comparativement à une copie profonde) tout en restant sûr.Types d'intersection
Les types d'intersection sont utiles pour décrire les types de fonctions surchargés : par exemple, si «des types de raffinement .
Types d'union
Dans une hiérarchie de sous-classes, l'union d'un type et d'un type ancêtre (tel que son parent) est le type ancêtre. L'union de 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
- intT = { une : int ; f : (int → int) ; }
- floatT = { a: float; f: (float → int); }
Ces types sont tous deux des sous-types du type existentiel plus général T et correspondent à des types d'implémentation concrets ; par conséquent, 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. Ceci offre une grande flexibilité dans le choix des types adaptés à une implémentation particulière, tandis que les clients qui utilisent uniquement des valeurs du type d'interface ( le type existentiel ) sont protégés de ces choix.
En général, il est impossible pour le vérificateur de types de déduire le type existentiel auquel appartient un module donné. Dans l'exemple ci-dessus, `intT { a: int; f: (int → int); }` pourrait également être de type `∃X { a: X; f: (X → int); }`. La solution la plus simple consiste à annoter chaque module avec son type attendu, par exemple :
- intT = { une : int ; f : (int → int) ; } comme ∃X { une : X ; f : (X → int) ; }
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 [de données] abstraits ont un type existentiel ». La théorie est un lambda-calcul typé du second ordre similaire au Système F , mais avec une quantification existentielle au lieu d'une quantification universelle.
Saisie progressive
Déclaration et inférence explicites ou implicites
virgule flottante , tandis qu'une autre peut impliquer une liste d'entiers (généralement un tableau) .L'inférence de types est généralement possible si elle est calculable dans le système de types considéré. De plus, même si l'inférence n'est pas calculable en général pour un système de types donné, elle est souvent possible pour une grande partie des programmes réels. Le système de types de Haskell, une version de Hindley-Milner , est une restriction du Système Fω aux types polymorphes de rang 1, pour 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 types impossible. (La vérification des types est cependant décidable , et les programmes de rang 1 bénéficient toujours de l'inférence de types ; les programmes polymorphes de rang supérieur sont rejetés sauf annotations de type explicites.)
Problèmes de décision
- Étant donné un environnement de type
- Étant donné un terme
- Étant donné un environnement de type
Système de types unifié
Certains langages, comme C# ou Scala, possèdent un système de types 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. D'autres langages, comme Java et Raku , possèdent un type racine, mais aussi des types primitifs qui ne sont pas des objets. Java fournit des types objets enveloppants qui coexistent avec les types primitifs, permettant ainsi aux développeurs d'utiliser indifféremment les types objets enveloppants ou les types primitifs non objets, plus simples. Raku convertit automatiquement les types primitifs en objets lors de l'accès à leurs méthodes.
Compatibilité : équivalence et sous-typage
Un vérificateur de types pour un langage statiquement typé doit s'assurer que le type de toute expression est cohérent avec le type attendu par le contexte dans lequel elle apparaît. Par exemple, dans une instruction d'affectation de la forme `x = x` , le type inféré de l'expression doit être cohérent avec le type déclaré ou inféré de la variable `x` . Cette notion de cohérence, appelée compatibilité , est spécifique à chaque langage de programmation.x:= eex
Si le type de `a` eet le type de `b` xsont identiques et que l'affectation est autorisée pour ce type, alors cette expression est valide. Ainsi, dans les systèmes de types les plus simples, la question de la compatibilité de deux types se réduit à celle de leur égalité (ou équivalence ). Cependant, les différents langages ont des critères différents pour déterminer quand deux expressions de type sont considérées comme désignant le même type. Ces différentes théories équationnelles des types varient considérablement ; deux cas extrêmes sont les systèmes de types structurels , où deux types décrivant des valeurs de même structure sont équivalents, et les systèmes de types nominatifs , où deux expressions de type syntaxiquement distinctes ne peuvent désigner 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 : si `T` Best un sous-type de ` AA`, alors une valeur de type `T` Bpeut être utilisée dans un contexte où une valeur de type ` A` Aest attendue ( covariance ), même si la réciproque n'est pas vraie. À l'instar de l'équivalence, la relation de sous-typage est définie différemment pour chaque langage de programmation, avec de nombreuses variations possibles. La présence de polymorphisme paramétrique ou ad hoc dans un langage peut également avoir des implications sur la compatibilité des types.