Règle de frappe

En théorie des types , une règle de typage est une règle d'inférence qui décrit comment un système de types attribue un type à une construction syntaxique . Ces règles peuvent être appliquées par le système de types pour déterminer si un programme est bien typé et quel type d'expression possède. Un exemple prototypique de l'utilisation des règles de typage est la définition de l'inférence de type dans le calcul lambda simplement typé , qui est le langage interne des catégories fermées cartésiennes .

Les règles de typage spécifient la structure d'une relation de typage qui relie les termes syntaxiques à leurs types. Syntactiquement, la relation de typage est généralement indiquée par deux points, ce qui indique par exemple qu'une expression est de type . Les règles elles-mêmes sont généralement spécifiées à l'aide de la notation de déduction naturelle . Par exemple, les règles de typage suivantes spécifient la relation de typage pour un langage simple de booléens :

Chaque règle stipule que la conclusion au-dessous de la ligne peut être déduite des prémisses au-dessus de la ligne. Les deux premières règles n'ont pas de prémisses au-dessus de la ligne, ce sont donc des axiomes . La troisième règle a des prémisses au-dessus de la ligne (plus précisément, trois prémisses), c'est donc une règle d'inférence .

Dans les langages de programmation, le type d'une variable dépend de l'endroit où elle est liée , ce qui nécessite des règles de typage sensibles au contexte. Ces règles sont données par un jugement de typage , généralement écrit , qui stipule qu'une expression a un type dans un contexte de typage qui relie les variables à leurs types. Les contextes de typage sont parfois complétés par les types de variables individuelles ; par exemple, peut être lu comme « le contexte complété par l'information que l'expression a un type donne le jugement que l'expression a un type ». Cette notation peut être utilisée pour donner des règles de typage pour les références de variables et l'abstraction lambda dans le calcul lambda simplement typé :

De même, la règle de typage suivante décrit la construction de Standard ML :

Tous les systèmes de règles de typage ne spécifient pas directement un algorithme de vérification de type . Par exemple, la règle de typage pour l'application d'une fonction paramétriquement polymorphe dans le système de types Hindley-Milner nécessite de « deviner » le type approprié auquel la fonction doit être instanciée. L'adaptation d'un système de règles déclaratives à un algorithme décidable nécessite la production d'un système algorithmique distinct dont on peut prouver qu'il spécifie la même relation de typage.