Types dépendants et substructurels

Les types dépendants permettent aux types de dépendre de valeurs, ce qui autorise des spécifications précises, tandis que les types substructurels, tels que les types linéaires et affines, contrôlent l'utilisation des ressources.

Definition

Les types dépendants sont des types qui dépendent de valeurs, permettant d'énoncer et de vérifier des propriétés précises au niveau du type ; les systèmes de types substructurels restreignent la manière dont les variables (ressources) peuvent être dupliquées ou supprimées, les types linéaires exigeant que chacune soit utilisée exactement une fois.

Scope

Ce sujet couvre des disciplines de typage avancées qui vont au-delà des systèmes conventionnels : les types dépendants, dans lesquels les types peuvent faire référence à des valeurs de programme, permettant ainsi aux types d'exprimer des spécifications complètes et de servir de preuves ; et les types substructurels (linéaires, affines, de propriété), qui restreignent les règles structurelles de contraction et d'affaiblissement pour suivre l'utilisation des ressources, l'aliasing et les durées de vie. Ce sujet est lié à la correspondance de Curry-Howard et aux assistants de preuve.

Core questions

• Comment les types peuvent-ils dépendre de valeurs pour exprimer des spécifications complètes de programme ?
• Quelle est la correspondance entre les types dépendants et les preuves constructives ?
• Comment les types linéaires et affines modélisent-ils les ressources, la propriété (ownership) et la sécurité de la mémoire ?
• Quels sont les compromis en termes de décidabilité et d'utilisabilité de ces systèmes riches ?

Key theories

Théorie des types intuitionniste (dépendante)

La théorie des types de Martin-Löf unifie la programmation et la logique constructive de sorte que les types sont des propositions et les programmes sont des preuves, fournissant ainsi la base des langages typés dépendamment et des assistants de preuve.

Logique linéaire et types linéaires

La logique linéaire de Girard affine la logique classique et intuitionniste en contrôlant les règles structurelles, et Wadler a montré comment les types linéaires basés sur celle-ci peuvent gérer en toute sécurité les mises à jour sur place et l'utilisation des ressources.

Statique pour les systèmes substructurels

Harper développe la métathéorie des systèmes de types substructurels et autres systèmes avancés dans un cadre uniforme de statique et de dynamique, clarifiant leur correction et leur interprétation des ressources.

Clinical relevance

Les types dépendants sont à la base des assistants de preuve et des logiciels vérifiés, où les programmes sont accompagnés de garanties de correction vérifiées par machine. Les types substructurels et de propriété (ownership) sous-tendent les langages système sûrs en matière de mémoire et de concurrence, permettant une gestion manuelle sûre des ressources sans collecteur de déchets.

History

La théorie des types intuitionniste de Martin-Löf (années 1970-1980) a établi les types dépendants et la vision des propositions comme types, menant à des assistants de preuve tels que Coq, Agda et Lean. La logique linéaire de Girard en 1987 a introduit le raisonnement sensible aux ressources ; les types linéaires de Wadler l'ont intégrée à la conception des langages, et les disciplines de propriété (ownership) et de vérification d'emprunt (borrow-checking) ont ensuite rendu les idées substructurelles courantes dans la programmation système.

Debates

Expressivité versus utilisabilité et décidabilité

Les systèmes typés dépendamment et substructurels peuvent exprimer des garanties très fortes, mais ils augmentent la charge de travail des programmeurs et peuvent rendre la vérification de type indécidable ou onéreuse, alimentant le débat sur la valeur de cette puissance par rapport à son coût.

Key figures

• Per Martin-Löf
• Jean-Yves Girard
• Philip Wadler
• Robert Harper

Seminal works

• martinlof1984
• girard1987
• wadler1990
• harper2016

Frequently asked questions

Qu'est-ce qu'un type dépendant ?

Un type dépendant est un type dont la définition dépend d'une valeur, comme le type des vecteurs d'une longueur spécifique, ce qui permet au système de types d'appliquer des invariants riches que les types ordinaires ne peuvent pas exprimer.

Que garantissent les types linéaires ?

Les types linéaires exigent que chaque valeur soit utilisée exactement une fois, ce qui permet à un compilateur d'autoriser en toute sécurité les mises à jour sur place, de gérer les ressources et de prévenir les erreurs liées à l'aliasing sans collecte de déchets à l'exécution.