Cette syntaxe, tandis qu'il peut sembler compliqué, est en fait assez simple. L'idée de base vient de la logique: l'expression entière est une implication avec la moitié supérieure étant les hypothèses et la moitié inférieure étant le résultat. C'est, si vous savez que le haut expressions sont vraies, vous pouvez en conclure que le fond expressions sont vraies.
Symboles
Une autre chose à garder à l'esprit est que certaines lettres ont traditionnel des significations; en particulier, Γ représente le "contexte" vous êtes-c'est ce que les autres types de choses que vous avez vu. Donc, quelque chose comme Γ ⊢ ... moyen ", l'expression" ... quand vous savez que les types de chaque expression en Γ.
L' ⊢ symbole signifie essentiellement que vous pouvez prouver quelque chose. Donc, Γ ⊢ ... est une déclaration disant: "je peux le prouver ... dans un contexte Γ. Ces déclarations sont également appelés type de jugements.
Une autre chose à garder à l'esprit: en mathématiques, tout comme ML et Scala, x : σ signifie qu' x type σ. Vous pouvez le lire comme Haskell x :: σ.
Ce que chaque règle signifie
Donc, sachant cela, la première expression devient facile à comprendre: si nous savons que l' x : σ ∈ Γ (c'est - x a un certain type σ dans certains contexte, Γ), alors nous savons qu' Γ ⊢ x : σ (qui est, en Γ, x type σ). Alors, vraiment, ce n'est pas en vous disant quelque chose de super-intéressant; il indique simplement comment utiliser votre contexte.
Les autres règles sont aussi simples. Prenez, par exemple, [App]. Cette règle a deux conditions: e₀ est une fonction à partir d'un certain type τ pour certains type τ' et e₁ est une valeur de type τ. Maintenant, vous savez quel type vous obtiendrez en appliquant e₀ de e₁! J'espère que ce n'est pas une surprise :).
La règle suivante a plus de nouvelle syntaxe. En particulier, Γ, x : τ signifie que le contexte constitué d' Γ , et le jugement x : τ. Donc, si nous savons que la variable x a un type d' τ et l'expression e a un type τ', nous avons également connaître le type d'une fonction qui prend en x et retours e. Cette juste nous dit quoi faire si nous avons compris ce type de fonction prend et le type de retours, donc il ne devrait pas être surprenant.
La prochaine on vous dit comment manipuler let des déclarations. Si vous savez que certains d'expression e₁ a un type τ tant que x a un type σ, puis un let expression qui localement se lie x pour une valeur de type σ feront e₁ avoir un type τ. Vraiment, cela vous indique que l'instruction let vous permet essentiellement d'étendre le contexte avec une nouvelle liaison qui est exactement ce qu' let !
L' [Inst] règle concerne le sous-typage. Il est dit que si vous avez une valeur de type σ' et c'est un sous-type d' σ (⊑ représente un partiel de la commande de rapport), alors que l'expression est également de type σ.
La règle finale traite avec la généralisation des types. Un rapide aparté: gratuitement une variable est une variable qui n'est pas introduite par un laisser-déclaration ou lambda à l'intérieur de certaines expression; cette expression dépend aujourd'hui de la valeur de la variable indépendante de son contexte.La règle est de dire que si y est une variable α qui n'est pas "libre" dans quoi que ce soit dans votre contexte, alors il est sûr de dire que toute expression dont le type que vous connaissez e : σ aura ce type pour toute valeur de α.
Comment utiliser les règles
Donc, maintenant que vous comprenez les symboles, que faites-vous avec ces règles? Eh bien, vous pouvez utiliser ces règles pour déterminer le type de valeurs différentes. Pour ce faire, regardez votre expression (disons f x y) et de trouver une règle qui a une conclusion (la partie inférieure) qui correspond à votre déclaration. Appelons-la chose que vous essayez de trouver votre "objectif". Dans ce cas, vous auriez l'air à la règle qui se termine en e₀ e₁. Lorsque vous avez trouvé cela, vous devez maintenant trouver des règles de prouver tout au-dessus de la ligne de cette règle. Ces choses correspondent généralement aux types de sous-expressions, de sorte que vous êtes essentiellement recursing sur les parties de l'expression. Vous venez de le faire jusqu'à la fin de votre preuve d'arbre, ce qui vous donne une preuve de la nature de votre expression.
Donc, toutes ces règles de faire est de spécifier exactement-et dans l'habitude mathématiquement pédant détail :P-comment déterminer les types d'expressions.
Maintenant, cela doit vous sembler familières si vous avez déjà utilisé Prolog-vous êtes essentiellement le calcul de la preuve de l'arbre comme un être humain interprète Prolog. Il y a une raison Prolog est appelé "programmation logique"! C'est aussi important que le premier moyen que j'ai été initié à la H-M algorithme d'inférence a été mise en œuvre dans Prolog. C'est en fait étonnamment simple et fait ce qu'il se passe clairement. Vous devriez certainement essayer.
Note: j'ai probablement fait quelques erreurs dans cette explication et l'aimerais si quelqu'un de vous les montrer. Je vais couvrir ce dans la classe à un couple de semaines, donc je vais être plus confiants alors :P.
