Système de type sous-structural - Substructural type system
| Systèmes de types |
|---|
| Concepts généraux |
| Principales catégories |
| Catégories mineures |
Les systèmes de types sous-structuraux sont une famille de systèmes de types analogues aux logiques sous-structurelles où une ou plusieurs règles structurelles sont absentes ou autorisées uniquement dans des circonstances contrôlées. De tels systèmes sont utiles pour restreindre l'accès aux ressources système telles que les fichiers , les verrous et la mémoire en gardant une trace des changements d'état qui se produisent et en empêchant les états invalides.
Différents types de systèmes de sous-structure
Plusieurs systèmes types ont émergé en écartant certaines des règles structurelles d'échange, d'affaiblissement et de contraction :
| Échanger | Affaiblissement | Contraction | Utilisation | |
|---|---|---|---|---|
| Commandé | - | - | - | Exactement une fois dans l'ordre |
| Linéaire | Autorisé | - | - | Exactement une fois |
| Affine | Autorisé | Autorisé | - | Au plus une fois |
| Pertinent | Autorisé | - | Autorisé | Au moins une fois |
| Normal | Autorisé | Autorisé | Autorisé | Arbitrairement |
- Systèmes de type ordonné (échange de rejet, affaiblissement et contraction) : Chaque variable est utilisée exactement une fois dans l'ordre où elle a été introduite.
- Systèmes de type linéaire (permettent l'échange, mais ni l'affaiblissement ni la contraction) : Chaque variable est utilisée exactement une fois.
- Systèmes de type affine (permettent l'échange et l'affaiblissement, mais pas la contraction) : Chaque variable est utilisée au plus une fois.
- Systèmes de type pertinents (permettent l'échange et la contraction, mais pas l'affaiblissement) : Chaque variable est utilisée au moins une fois.
- Systèmes de type normal (permettent l'échange, l'affaiblissement et la contraction) : Chaque variable peut être utilisée arbitrairement.
L'explication des systèmes de type affine est mieux comprise si elle est reformulée comme "chaque occurrence d'une variable est utilisée au plus une fois".
Système de type ordonné
Les types ordonnés correspondent à une logique non commutative où l'échange, la contraction et l'affaiblissement sont écartés. Cela peut être utilisé pour modéliser l' allocation de mémoire basée sur la pile (contrairement aux types linéaires qui peuvent être utilisés pour modéliser l'allocation de mémoire basée sur le tas). Sans la propriété d'échange, un objet ne peut être utilisé qu'en haut de la pile modélisée, après quoi il est supprimé, ce qui fait que chaque variable est utilisée exactement une fois dans l'ordre dans lequel elle a été introduite.
Systèmes de type linéaire
Les types linéaires correspondent à la logique linéaire et garantissent que les objets sont utilisés exactement une fois, permettant au système de désallouer en toute sécurité un objet après son utilisation.
Le langage de programmation Clean utilise des types d'unicité (une variante des types linéaires) pour aider à prendre en charge la concurrence, les entrées/sorties et la mise à jour sur place des tableaux.
Les systèmes de type linéaire autorisent les références mais pas les alias . Pour appliquer cela, une référence sort de la portée après son apparition sur le côté droit d'une affectation , garantissant ainsi qu'une seule référence à un objet existe à la fois. Notez que passer une référence en tant qu'argument à une fonction est une forme d'affectation, car le paramètre de fonction se verra affecter la valeur à l'intérieur de la fonction, et donc une telle utilisation d'une référence la fait également sortir de la portée.
Un système de type linéaire est similaire à C ++ de unique_ptr classe , qui se comporte comme un pointeur , mais ne peut être déplacé ( par exemple non copiés) dans une affectation. Bien que la contrainte de linéarité soit vérifiée au moment de la compilation , le déréférencement d'un unique_ptr invalidé entraîne un comportement indéfini au moment de l' exécution .
La propriété de référence unique rend les systèmes de type linéaire appropriés comme langages de programmation pour le calcul quantique , car elle reflète le théorème de non-clonage des états quantiques. Du point de vue de la théorie des catégories , le non-clonage est une déclaration selon laquelle il n'y a pas de foncteur diagonal qui pourrait dupliquer des états ; de même, du point de vue du combinateur , il n'y a pas de K-combinateur qui puisse détruire des états. Du point de vue du lambda calcul , une variable x peut apparaître exactement une fois dans un terme.
Les systèmes de types linéaires sont le langage interne des catégories monoïdales symétriques fermées , de la même manière que le lambda-calcul simplement typé est le langage des catégories fermées cartésiennes . Plus précisément, on peut construire des foncteurs entre la catégorie des systèmes de types linéaires et la catégorie des catégories monoïdales symétriques fermées.
Systèmes de type affine
Les types affines sont une version des types linéaires permettant de supprimer (c'est-à-dire de ne pas utiliser ) une ressource, correspondant à la logique affine . Une ressource affines peut être utilisé au plus une fois, tandis qu'un linéaire doit être utilisé exactement une fois.
Système de type pertinent
Les types pertinents correspondent à une logique pertinente qui permet l'échange et la contraction, mais pas l'affaiblissement, ce qui se traduit par le fait que chaque variable est utilisée au moins une fois.
Langages de programmation
Les langages de programmation suivants prennent en charge les types linéaires ou affines :
Voir également
Remarques
Les références
- Walker, David (2002). "Systèmes de type sous-structural". Dans Pierce, Benjamin C. (éd.). Sujets avancés dans les types et les langages de programmation (PDF) . Presse MIT. p. 3-43. ISBN 0-262-16228-8.