Qu’est-ce que le typage dépendant?

Est-ce que quelqu’un peut m’expliquer la dactylographie dépendante? J’ai peu d’expérience dans les langages Haskell, Cayenne, Epigram ou autres langages fonctionnels, donc plus les termes que vous pouvez utiliser sont simples, plus je l’apprécierai!

Considérez ceci: dans tous les langages de programmation décents, vous pouvez écrire des fonctions, par exemple

def f(arg) = result 

Ici, f prend une valeur arg et calcule un result valeur. C’est une fonction des valeurs aux valeurs.

Maintenant, certains langages vous permettent de définir des valeurs polymorphes (aka génériques):

 def empty = new List() 

Ici, empty prend un type T et calcule une valeur. C’est une fonction des types aux valeurs.

En général, vous pouvez également avoir des définitions de type génériques:

 type Masortingx = List> 

Cette définition prend un type et renvoie un type. Il peut être considéré comme une fonction des types aux types.

Tellement pour ce que les langues ordinaires offrent. Un langage est appelé typé de manière dépendante s’il offre également la 4ème possibilité, à savoir la définition des fonctions des valeurs aux types. Ou en d’autres termes, paramétrer une définition de type sur une valeur:

 type BoundedInt(n) = {i:Int | i<=n} 

Certaines langues dominantes ont une fausse forme à ne pas confondre. Par exemple, en C ++, les modèles peuvent prendre des valeurs en tant que parameters, mais ils doivent être des constantes à la compilation lorsqu'ils sont appliqués. Ce n'est pas le cas dans un langage vraiment dépendant. Par exemple, je pourrais utiliser le type ci-dessus comme ceci:

 def min(i : Int, j : Int) : BoundedInt(j) = if i < j then i else j 

Ici, le type de résultat de la fonction dépend de la valeur d'argument réelle j , donc de la terminologie.

Si vous connaissez le C ++, il est facile de fournir un exemple motivant:

Disons que nous avons un type de conteneur et deux instances de celui-ci

 typedef std::map IIMap; IIMap foo; IIMap bar; 

et considérez ce fragment de code (vous pouvez supposer que foo est non vide):

 IIMap::iterator i = foo.begin(); bar.erase(i); 

C’est une erreur évidente (et qui corrompt probablement les structures de données), mais elle va taper à la IIMap::iterator car “iterator into foo” et “iterator into bar” sont du même type, IIMap::iterator , même si elles sont totalement incompatibles sémantiquement.

Le problème est qu’un type d’iterator ne doit pas dépendre uniquement du type de conteneur mais en fait de l’ object conteneur, c’est-à-dire qu’il doit s’agir d’un “type de membre non statique”:

 foo.iterator i = foo.begin(); bar.erase(i); // ERROR: bar.iterator argument expected 

Une telle fonctionnalité, la capacité d’exprimer un type (foo.iterator) qui dépend d’un terme (foo), est exactement ce que signifie le typage dépendant.

La raison pour laquelle vous ne voyez pas souvent cette fonctionnalité est qu’elle ouvre une grande boîte de vers: vous vous retrouvez soudainement dans des situations où, pour vérifier au moment de la compilation si deux types sont identiques, vous devez prouver deux expressions. sont équivalents (donneront toujours la même valeur à l’exécution). Par conséquent, si vous comparez la liste de langages de typage dépendant de wikipedia avec sa liste de démonstrateurs de théorèmes, vous remarquerez peut-être une similitude suspecte. 😉

Citant le livre Types et langages de programmation (30.5):

Une grande partie de ce livre a été consacrée à la formalisation de mécanismes d’abstraction de diverses sortes. Dans le lambda-calcul simplement typé, nous avons formalisé l’opération de prendre un terme et d’extraire un sous-terme, produisant une fonction qui peut être instanciée ultérieurement en l’appliquant à des termes différents. Dans le système F , nous avons considéré l’opération consistant à prendre un terme et à en extraire un type, en produisant un terme qui peut être instancié en l’appliquant à différents types. Dans λω , nous avons récapitulé les mécanismes du lambda-calcul simplement typé «one level up», en prenant un type et en soustrayant une sous-expression pour obtenir un opérateur de type qui peut être instancié ultérieurement en l’appliquant à différents types. Une manière commode de penser toutes ces formes d’abstraction est en termes de familles d’expressions, indexées par d’autres expressions. Une abstraction lambda ordinaire λx:T1.t2 est une famille de termes [x -> s]t1 indexés par les termes s . De même, une abstraction de type λX::K1.t2 est une famille de termes indexés par types, et un opérateur de type est une famille de types indexés par types.

  • λx:T1.t2 famille de termes λx:T1.t2 indexés par termes

  • Famille de termes λX::K1.t2 indexés par types

  • Famille de types λX::K1.T2 indexés par types

En regardant cette liste, il est clair qu’il existe une possibilité que nous n’avons pas encore envisagée: les familles de types indexés par termes. Cette forme d’abstraction a également été étudiée de manière approfondie, sous la rubrique des types dépendants.

Les types dépendants permettent d’éliminer un plus grand nombre d’ erreurs logiques au moment de la compilation . Pour illustrer cela, considérons la spécification suivante sur la fonction f :

La fonction f doit prendre que des entiers pairs en entrée.

Sans types dépendants, vous pourriez faire quelque chose comme ceci:

 def f(n: Integer) := { if n mod 2 != 0 then throw RuntimeException else // do something with n } 

Ici, le compilateur ne peut pas détecter si n est en effet même, c’est-à-dire que du sharepoint vue du compilateur, l’expression suivante est correcte:

 f(1) // comstacks OK despite being a logic error! 

Ce programme s’exécuterait puis lancerait une exception à l’exécution, c’est-à-dire que votre programme a une erreur logique.

Maintenant, les types dépendants vous permettent d’être beaucoup plus expressif et vous permettent d’écrire quelque chose comme ceci:

 def f(n: {n: Integer | n mod 2 == 0}) := { // do something with n } 

Ici n est de type dépendant {n: Integer | n mod 2 == 0} {n: Integer | n mod 2 == 0} . Il pourrait être utile de lire ceci à haute voix

n est membre d’un ensemble d’entiers tel que chaque entier est divisible par 2.

Dans ce cas, le compilateur détectera au moment de la compilation une erreur logique où vous avez passé un nombre impair à f et empêché l’exécution du programme:

 f(1) // comstackr error