Comment faut-il lire la notation des systèmes de types ?

• Cet article propose une explication détaillée de la manière de lire et de comprendre la notation des systèmes de types dans les langages de programmation.
• La notation des systèmes de types est une expression mathématique utilisée dans les articles ou les publications scientifiques consacrés aux systèmes de types.
• La notation utilisée pour décrire un système de types varie selon les présentations, mais la plupart partagent de nombreux éléments communs.
• Un système de types appliqué à un langage de programmation est un système syntaxique, c’est-à-dire un ensemble de règles qui s’appliquent à la syntaxe du langage.
• Cette notation trouve son origine dans la logique formelle et sert à construire des preuves formelles des propriétés d’un système.
• Cet article aborde également les notions de relation, de jugement, d’axiome et de règle d’inférence dans la notation des systèmes de types.
• La relation de typage s’écrit généralement e:τ et peut se lire « e a le type τ ».
• Un jugement de typage s’écrit avec la notation ⊢e:τ⊢, où ⊢ peut se lire comme « l’énoncé suivant est vrai ».
• Cet article explique aussi en détail les notions de variable, de contexte et d’environnement dans la notation des systèmes de types.
• Le contexte, ou environnement de types, est représenté par Γ dans cette notation.
• L’article couvre également d’autres notations et points d’attention courants, comme la présentation des règles d’inférence, les conditions latérales, le sous-typage, les contextes multiples et la vérification de types bidirectionnelle.
• Cet article constitue un guide complet pour comprendre la notation des systèmes de types, en particulier pour les personnes qui découvrent ce concept.

[GN⁺]

Discussion Hacker News

• Discussion sur la notation des systèmes de types dans les articles d’informatique théorique, avec une explication de base de la notation BNF, des règles d’inférence, etc.
• L’origine de cette notation remonterait à Frege, avec comme éléments clés le symbole de tourniquet et la barre horizontale
• Bien qu’ils aient étudié l’informatique, certains lecteurs trouvent encore déroutants |- et |=, ainsi que le sens, au niveau méta-syntaxique, des variables utilisées
• Certains remercient pour l’explication, mais se demandent aussi pourquoi elle a été rédigée sur Stack Exchange plutôt que sur une autre plateforme comme lexi-lambda.github.io
• Types and Programming Languages de Benjamin C. Pierce est recommandé comme un bon manuel sur le sujet
• Certains lecteurs disent s’être interrogés pendant des années sur ce sujet sans savoir comment l’aborder
• L’Ada Reference Manual est mentionné comme un exemple d’usage pratique de ce type de syntaxe
• Des éloges sont adressés à cette réponse qui part des bases avant de monter progressivement en complexité
• 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 est absurde dans la plupart des langages, mais en Python, True + 2 est bien un entier et vaut 3, ce qui est donné en exemple