Comment lire la notation des systèmes de types ?

 (langdev.stackexchange.com)
1 points par GN⁺ 2023-08-17 | 1 commentaires | Partager sur WhatsApp
  • Même si la notation des systèmes de types varie selon les documents, connaître le cadre commun — grammaire, relation de typage et règles d’inférence — permet de suivre la plupart des variantes
  • Un système de types opère sur la syntaxe abstraite d’un langage ; il faut donc d’abord distinguer, dans la grammaire, les termes (term) qui ont un type et les types eux-mêmes
  • ⊢ e: τ est un jugement de typage signifiant « l’expression e a le type τ » ; il se lit comme une règle d’inférence où, si toutes les conditions au-dessus de la barre horizontale sont vraies, alors la conclusion en dessous l’est aussi
  • Avec l’introduction de variables et de fonctions, on ajoute un contexte, comme dans Γ ⊢ e: τ, afin de suivre les noms de variables et leurs types dans la portée courante
  • Beaucoup de règles de typage peuvent se lire comme une fonction récursive de vérification de types, mais tout jugement logique ne se transforme pas directement en algorithme de vérification de types décidable

La notation des systèmes de types part de la grammaire

  • Un système de types est un système syntaxique d’un langage de programmation : un ensemble de règles qui opèrent sur la syntaxe abstraite du langage
  • Une description complète d’un système de types commence généralement par présenter les structures syntaxiques concernées sous forme de grammaire, souvent avec la notation BNF
  • Même dans le langage typé le plus simple, la syntaxe se divise en deux grandes catégories
    • e : les expressions qui ont un type
    • τ : les types attachés aux expressions
  • Le langage d’exemple possède comme expressions des littéraux booléens, des littéraux entiers, des expressions conditionnelles, des opérations arithmétiques et des comparaisons, et utilise Bool et Int comme types
  • Selon les documents, le symbole de type peut être écrit t, T, σ ou avec d’autres lettres grecques minuscules au lieu de τ, mais la structure générale reste similaire
  • Les langages plus complexes peuvent inclure davantage de catégories syntaxiques, comme les instructions ou les motifs de pattern matching

Lire les relations et jugements de typage

  • Après avoir défini la grammaire, on définit généralement une relation de typage de la forme e : τ
    • 1 + 2 : Int signifie que « 1 + 2 est de type Int »
    • 1 + 2 : Bool affirme que la même expression est de type Bool, ce qui est incorrect
    • true + 2 : Int n’a pas de sens en tant qu’expression et n’a donc aucun type
  • ⊢ e : τ est un jugement de typage, et ⊢ peut se lire comme « l’énoncé qui suit est vrai »
  • Une règle qui n’a rien au-dessus de la barre horizontale est un axiome, toujours vrai
    • ⊢ true : Bool
    • ⊢ false : Bool
    • Les règles pour les littéraux entiers, comme ⊢ 0 : Int, ⊢ 1 : Int, ⊢ -1 : Int
  • Une règle avec des éléments au-dessus et en dessous de la barre est une règle d’inférence
    • Si toutes les conditions au-dessus sont vraies, alors la conclusion en dessous est vraie
    • Si e₁ et e₂ sont tous deux de type Int, alors e₁ + e₂ est de type Int
    • Si e₁ et e₂ sont tous deux de type Int, alors e₁ < e₂ est de type Bool

Expressions conditionnelles et variables de type

  • Les deux branches de if ... then ... else ... peuvent être de n’importe quel type, mais elles doivent avoir le même type
    • if true then 1 else 2 est possible
    • if true then false else true est possible
    • if true then 1 else true est impossible
  • Pour l’exprimer, la règle utilise une variable τ représentant le type des branches
    • L’expression conditionnelle e₁ doit être de type Bool
    • La branche then e₂ et la branche else e₃ doivent avoir le même type τ
    • Le type de l’expression conditionnelle entière est aussi τ
  • Lorsqu’on applique la règle, on peut choisir n’importe quel type pour τ, mais il faut conserver ce choix de manière cohérente dans la même règle

Lire les règles d’inférence comme un algorithme

  • Cette notation vient de la logique formelle, et la manière de spécifier les systèmes de types ressemble particulièrement à la déduction naturelle
  • Ces règles servent à construire des preuves formelles sur les propriétés du système, et sont importantes pour prouver des propriétés comme la sûreté de typage
  • Un jugement logique ne correspond pas toujours directement à un algorithme de vérification de types décidable
  • Dans de nombreux cas, on peut lire ⊢ e : τ comme une fonction qui obtient le type τ à partir de l’expression e
    • Il existe généralement une règle pour chaque forme d’expression de la grammaire
    • Chaque règle de typage peut être vue comme une branche d’une fonction récursive de vérification de types
  • La fonction infer de l’exemple correspond au déroulé suivant
    • true ou false donne Bool
    • Un littéral entier donne Int
    • e₁ + e₂ donne Int après avoir vérifié que les résultats d’inférence des deux côtés sont tous deux Int
    • e₁ < e₂ donne Bool après avoir vérifié que les deux côtés sont de type Int
    • if e₁ then e₂ else e₃ vérifie que la condition est de type Bool, puis que les deux branches ont le même type, et renvoie ce type
  • Même lorsqu’il n’est pas possible de le transformer directement en algorithme, considérer e comme une entrée et τ comme une sortie dans le jugement facilite la compréhension du flux d’information

Variables et contexte

  • Pour traiter des langages de programmation utiles, il faut des variables ; l’exemple est étendu avec des fonctions pour prendre la forme du lambda-calcul simplement typé
  • La grammaire étendue inclut les éléments suivants
    • Variable x
    • Abstraction de fonction λx:τ. e
    • Application de fonction e e
    • Type fonction τ → τ
  • λx:τ. e correspond à (x:τ) => e en TypeScript, et f x correspond à f(x)
  • Le type d’une variable dépend du contexte dans lequel elle apparaît ; on ne peut donc pas écrire une règle sous la simple forme ⊢ x : ???
  • Le jugement de typage est donc étendu en Γ ⊢ e : τ
    • Γ est le contexte, ou environnement de types
    • ⊢ sépare les hypothèses contextuelles à gauche de l’énoncé à prouver à droite
    • Il se lit : « sous le contexte Γ, l’expression e a le type τ »
  • Algorithmiquement, Γ peut être vu comme une entrée supplémentaire de la forme Map<Variable, Type>
  • Formellement, le contexte est lui aussi spécifié comme une structure syntaxique
    • ∅ : contexte vide
    • Γ, x:τ : contexte auquel on a ajouté un binding de variable
    • Parfois, • est utilisé comme contexte vide au lieu de ∅
  • Dans cette représentation, le contexte ressemble à une liste d’association qui associe des noms de variables à des types

Le rôle du contexte dans les règles

  • Beaucoup de règles de typage transmettent le contexte tel quel, sans le modifier
    • Γ ⊢ true : Bool
    • Si Γ ⊢ e₁ : Int et Γ ⊢ e₂ : Int, alors Γ ⊢ e₁ + e₂ : Int
  • Le contexte joue un rôle central dans les règles d’utilisation des variables et des lambdas
    • Si x:τ ∈ Γ, alors Γ ⊢ x : τ
    • Si Γ, x:τ₁ ⊢ e : τ₂, alors Γ ⊢ (λx:τ₁. e) : τ₁ → τ₂
  • Lorsqu’on vérifie le type du corps e d’une lambda, le contexte est étendu avec le nouveau binding x:τ₁
  • La règle des variables juge que, si un binding de variable existe dans le contexte courant, cette variable a le type correspondant
  • Le contexte sert de mécanisme de communication entre la règle des lambdas et la règle des variables
  • Pour simplifier, les spécifications de systèmes de types de ce genre supposent généralement que toutes les variables ont déjà été résolues et rendues uniques, et ne traitent pas le masquage de variables
  • La règle d’application de fonction vérifie conjointement le type de l’expression de fonction et celui de l’expression argument
    • e₁ doit être de type τ₁ → τ₂
    • e₂ doit être de type τ₁
    • Le type de l’application complète e₁ e₂ devient τ₂

Notations supplémentaires fréquentes

  • Les règles d’inférence ne sont pas toujours écrites uniquement à la verticale
    • Plusieurs conditions peuvent être disposées côte à côte horizontalement
    • Les dispositions verticales et horizontales peuvent être mélangées dans une même règle
  • Les conditions au-dessus de la barre sont généralement d’autres jugements, mais il peut aussi s’agir de conditions annexes (side conditions) booléennes arbitraires
    • x:τ ∈ Γ dans la règle des variables en est un exemple
    • Dans les systèmes de types algorithmiques, on peut voir α fresh, qui signifie que α doit être une nouvelle variable de type, distincte des autres variables de type

Sous-typage

  • Le sous-typage est une relation qui traite la compatibilité entre types de manière moins stricte que l’égalité exacte, et doit être défini explicitement
  • Il s’écrit généralement τ₁ <: τ₂ et se lit : « τ₁ est un sous-type de τ₂ »
  • Une relation de sous-typage simple peut introduire un type sommet ⊤ et un type fond ⊥
    • τ <: τ : tout type est un sous-type de lui-même
    • τ <: ⊤ : tout type est un sous-type de ⊤
    • ⊥ <: τ : ⊥ est un sous-type de tout type
  • La première règle est la règle de réflexivité, souvent abrégée en refl
  • Pour autoriser le sous-typage, il faut utiliser explicitement cette relation dans chaque règle de typage qui l’accepte
    • Dans la règle d’application de fonction, on peut autoriser l’application si le type de l’argument τ₁ est un sous-type du type du paramètre τ₂

Contextes multiples et vérification bidirectionnelle des types

  • Certains systèmes de types définissent des jugements de typage comportant plusieurs contextes
    • Le second contexte est généralement appelé Δ
    • Γ;Δ ⊢ e : τ est souvent utilisé lorsque les deux contextes servent d’entrées
    • Γ ⊢ e : τ ⊣ Δ est souvent utilisé lorsque Δ sert de sortie
  • Le second contexte est utilisé différemment selon les cas
    • Il peut permettre de ne référencer certaines variables qu’à l’intérieur d’une expression donnée
    • Dans les langages de programmation sensibles aux ressources, il peut servir de contexte de sortie pour suivre les variables qui ont été consommées
  • La vérification bidirectionnelle des types est une approche qui réalise une inférence de types non locale limitée sans solveur de contraintes
  • Les systèmes bidirectionnels divisent le jugement général Γ ⊢ e : τ en deux jugements spécialisés
    • Γ ⊢ e ⇐ τ : jugement de vérification (checking) qui vérifie que l’expression e a le type attendu τ ; algorithmiquement, τ est une entrée
    • Γ ⊢ e ⇒ τ : jugement d’inférence utilisé lorsqu’il n’y a pas d’information de type attendue ; algorithmiquement, τ est une sortie
  • Les deux jugements sont définis par récursion mutuelle et propagent l’information de type dans les deux directions
  • Avec cette approche, certaines annotations de type peuvent être omises ; la règle de vérification des abstractions lambda peut obtenir le type du paramètre à partir du type fonction attendu, ce qui permet d’omettre l’annotation du binder de variable

À lire aussi

1 commentaires

 
GN⁺ 2023-08-17
Avis sur Hacker News

  • Guy Steele avait déjà donné une présentation sur ce sujet. Il avait même donné à certaines notations des noms qu’on peut rechercher, comme diagrammes bidimensionnels de règles d’inférence
    Il appelle cela une métanotation pour l’informatique, mais personnellement, ça me semble plus proche de la théorie des langages de programmation. https://m.youtube.com/watch?v=dCuZkaaou0Q

  • Cette notation remonte jusqu’à Frege. C’est difficile à chercher si l’on ne sait pas quoi chercher, mais cet article semble être un assez bon résumé : https://plato.stanford.edu/entries/frege-logic
    Le symbole de tourniquet |- était déjà utilisé, et la ligne horizontale qu’on appelait en cours « Fregescher Schlussstrich », c’est-à-dire le trait de conclusion de Frege, semble avoir fait à l’origine partie du tourniquet lui-même avant de devenir un élément séparé dans la notation moderne

    • « Schlussstrich » se traduirait sans doute plutôt par trait de déduction ou trait d’inférence

  • Types and Programming Languages de Benjamin C. Pierce est un bon manuel qui couvre ce genre de choses

    • C’est ironique, parce que TAPL est assez peu clair quand il s’agit d’expliquer le sens de base de la syntaxe qu’il utilise lui-même. Cette réponse est plusieurs ordres de grandeur plus claire que TAPL

  • Même en ayant fait des études d’informatique, je suis toujours embrouillé par la différence de sens entre |– et |=, et par le niveau de métasyntaxe auquel se trouvent chacune des variables utilisées
    Ironiquement, l’une des causes est que la notation elle-même n’a pas de types explicites

  • Pour ceux qui hésitent à lire : cet article explique la notation des systèmes de types qu’on trouve dans les articles d’informatique, et c’est en fait une introduction à la notation BNF, aux règles d’inférence, etc. pour les systèmes de types
    Ça ressemble à un bon résumé

    • Honnêtement, il me suffirait d’une antisèche indiquant comment lire les symboles en mots anglais
      Je comprends le concept logique de l’application des types, mais comme je ne lis pas souvent des articles d’informatique, l’association entre les symboles et leur sens ne se fixe pas bien dans ma tête
    • Le fait que ce genre de chose ait été abstrait de manière aussi poussée au fil des années montre bien le côté très informatique de la discipline

  • Dans les exemples, 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 signifie « 𝗍𝗋𝗎𝖾+2 est de type 𝖨𝗇𝗍 », mais il est dit que c’est d’autant plus étrange que l’expression 𝗍𝗋𝗎𝖾+2 elle-même n’a pas de sens et n’a pas non plus de type
    Pourtant, en Python, True + 2 est bel et bien un entier, et sa valeur est 3. Que cela doive être le cas ou non est une autre question, mais dans les faits c’est ainsi

    • Si l’on considère que True + 2 a du sens, il suffit de définir soi-même une règle de jugement qui l’autorise
      La logique et la théorie des systèmes de types ne s’intéressent pas en soi aux axiomes et règles d’inférence que l’on choisit ; elles permettent seulement de raisonner sur ces règles et leurs interactions. Par exemple, on peut poser |- True : Bool, |- True : Int, ou, si l’on veut ne l’autoriser que dans certaines expressions, faire dériver |- True + x: Int à partir de |- x : Int
    • Cela ne dépend-il pas du langage ? Par exemple en C, true est mappé sur 1, donc true+1=2
    • Même si True + 2 ne produit pas d’erreur en Python ou en C, cela reste idiot, parce qu’on rend la sémantique du langage plus difficile à raisonner juste pour donner un peu de sucre syntaxique au programmeur

  • Très bien. Cela faisait des années que je me posais la question, mais je ne savais pas quels mots-clés utiliser pour en savoir plus

  • Parfois, quand quelqu’un publie gratuitement un savoir ésotérique qu’on a eu du mal à acquérir, on se sent bêtement contrarié ;) J’aurais vraiment aimé avoir ce genre d’article quand j’apprenais cela. J’espère qu’une meilleure accessibilité réduira le nombre de langages mal fichus

  • En lisant l’Ada Reference Manual, j’ai immédiatement reconnu ce genre de syntaxe. Je n’en connaissais pas le nom, mais c’était intéressant de la voir dans un cas d’usage réel, et tout le langage est défini avec cette notation
    Exemple : https://ada-lang.io/docs/arm/AA-3/AA-3.7#syntax

  • Ça me semble être un bon endroit pour prêcher en faveur d’une colline sur laquelle j’ai décidé de mourir. Dans le format d’annotation de type qui utilise deux-points, les espaces de part et d’autre du deux-points devraient être identiques
    Pour moi, il se trouve simplement qu’il existe deux signes différents qui ont la même apparence, à savoir deux points superposés. L’un est le deux-points d’étiquette, où, comme en anglais, la partie précédente introduit la suivante, ou la gauche est l’étiquette de la droite ; c’est le cas du début de bloc en Python, des paires clé-valeur, ou des paires nom-valeur dans les structs en C ou Rust
    L’autre est l’annotation de type empruntée aux mathématiques. C’est une relation binaire, et les relations binaires prennent le même espacement à gauche et à droite. De même qu’on n’écrit pas x= 1, x> y ou x+ z, il est plus naturel d’écrire x : X plutôt que x: X
    Quand je vois a: b, je le lis immédiatement comme un deux-points d’étiquette, et lorsqu’il s’agit d’une annotation de type, cela demande à chaque fois une conversion mentale supplémentaire, minuscule mais réelle. Je parle ici de syntaxe de langages de programmation, et personnellement je préfère de loin x : X à X x
    [1] « Evangelion » est un mot élégant qui vient de εὐαγγέλιον, c’est-à-dire « bonne nouvelle ». [2] https://en.wikipedia.org/wiki/Colon_(punctuation)#Usage_in_E...

    • Il peut y avoir quelques malentendus. Même dans l’écriture mathématique, on voit effectivement des notations comme f: X->Y, avec plus d’espace à droite du deux-points ; sur les 3 livres que j’ai vérifiés, 1 n’utilisait que cette notation
      De plus, cela reste assez proche d’un étiquetage : on étiquette un morphisme d’une forme donnée. Le cas où, en mathématiques, le deux-points a vraiment un autre sens, c’est lorsqu’il sert d’abréviation de such that, par exemple dans des définitions d’ensembles comme { x : x \in IN and x | 2}, ou souvent avec des quantificateurs
    • Point de vue intéressant. Ce que tu dis à propos de l’étape mentale supplémentaire correspond à ce que je ressens quand je lis la notation courante X x. x: X me paraît beaucoup plus naturel, et plus proche aussi de la façon dont on utilise le deux-points en langue naturelle
      Il y a une proposition, et ce qui suit le deux-points l’explique plus en détail ; comme le type est lui aussi une information supplémentaire sur ce qui se trouve à gauche, ça colle parfaitement
    • En théorie des types, je considère que la pratique standard est généralement de mettre le même espace des deux côtés du deux-points, comme dans t[espace]:[espace]T
      La théorie des types dans son ensemble a des aspects incohérents et assez brouillons, mais c’est l’un des rares cas où tout le monde est plutôt cohérent. Par curiosité, j’ai regardé comment je l’écrivais à l’époque de la licence, et je l’avais moi aussi écrit joliment de façon symétrique : https://dvt.name/logic/horse2.pdf
    • x: X correspond à l’usage où « une explication vient après le deux-points »
      Autrement dit, quelque chose comme variable x: It’s an X.
    • age: int se reformule facilement en anglais comme « person’s age: an integer »
      C’est pourquoi le deux-points ne m’a jamais vraiment gêné