Aide à la compréhension de la notation académique pour le système de type

Question

J'essaie de comprendre un academic paper (pdf) sur la conception du langage de programmation. En particulier, il décrit une version légère de Java appelée Featherweight Java. Il a des règles de typage avec la notation comme ceci:

x_ : C_, this : C |- e0 : E0   E0 <: C0 
class C extends D {...} 
if mtype(m,D) = D_->D0, then C_ = D_ and C0 = D0 
--------------------------------------------------------------------------- 
C0 m(C_ x_){ return e0; } OK IN C 

C'est ma meilleure tentative de le reproduire dans le texte, de toute façon. Cependant, l'article semble supposer qu'une telle notation est familière et l'explique à peine. Quelqu'un pourrait-il me diriger vers une meilleure explication? Merci!

Answer 1

On dirait formal semantics, et dans ce cas de syntaxe probablement denotational semantics, mais certains symboles semblent plutôt cryptiques.

Answer 2

Le manuel de premier cycle de Benjamin Pierce Types and Programming Languages vous apprendra tout ce que vous devez savoir pour comprendre les notations utilisées dans le papier Java Featherweight. (Je pense que Pierce peut aussi être co-auteur de ce document.)

Answer 3

Ceci est un exemple particulièrement compliqué, et quelques choses distinctes se passent à l'intérieur.

La notation en barre horizontale est généralement utilisée pour les règles d'inférence . Au-dessus de la ligne sont les locaux (généralement séparés par des espaces sur une seule ligne), en dessous de la ligne est une conclusion. Par exemple,

P0 P1 ... Pn 
------------------ 
     C 

signifie « si P0 par Pn tous tiennent, nous pouvons conclure que C tient aussi bien. »

La notation de tourniquet (⊦) est habituellement utilisée pour les relations d'implication . Dans les systèmes de type, cela signifie généralement que "si nous supposons les types sur le côté gauche, nous pouvons dériver les types sur le côté droit." Le côlon est classiquement utilisé pour associer une variable ou une expression avec un type, donc

x_ : C_, this : C ⊦ e0 : E0 

moyens "Suppose x_ est de type C_ et this est de type C, on peut en déduire que e0 est de type E0." ¹

Le symbole <: est classiquement utilisé pour les relations de sous-typage, mais ce devrait être défini explicitement dans l'article.

Le bit "class C extends D" semble faire référence à la syntaxe du programme source. C'est-à-dire, la prémisse prévue est "C est explicitement déclaré pour étendre D".

Le reste est difficile à graver sans patauger dans le papier. Je suis profondément d'accord avec la recommandation de Norman Ramsey de Pierce comme une bonne introduction à la théorie des types. ¹ Notez que la différence entre "inférence" et "implication" est soit subtile, soit inexistante - laquelle doit être utilisée pour les conventions, les goûts et/ou les distinctions fines.