Je jure qu'il y avait un T-shirt à vendre avec les mots immortels:

Quelle partie de

tu ne comprends pas ?

Dans mon cas, la réponse serait ... tout!

En particulier, je vois souvent une notation comme celle-ci dans les articles de Haskell, mais je n'ai aucune idée de ce que cela signifie. Je n'ai aucune idée de quelle branche des mathématiques c'est censé être.

Je reconnais bien sûr les lettres de l'alphabet grec et des symboles tels que "∉" (ce qui signifie généralement que quelque chose n'est pas un élément d'un ensemble).

D'un autre côté, je n'ai jamais vu "⊢" auparavant ( Wikipedia prétend que cela pourrait signifier "partition" ). Je ne connais pas non plus l'utilisation du vinculum ici. (Habituellement, cela dénote une fraction, mais cela ne semble pas être le cas ici.)

Si quelqu'un pouvait au moins me dire par où commencer pour chercher à comprendre ce que cette mer de symboles signifie, ce serait utile.

• La barre horizontale signifie que "[ci-dessus] implique [ci-dessous]".
• S'il y a plusieurs expressions dans [ci-dessus], alors considérez-les et regroupées; toutes les [ci-dessus] doivent être vraies afin de garantir le [ci-dessous].
• :signifie a type
• ∈signifie est . (De même, ∉signifie «n'est pas dedans».)
• Γest généralement utilisé pour faire référence à un environnement ou un contexte; dans ce cas, il peut être considéré comme un ensemble d'annotations de type, associant un identifiant à son type. Signifie donc x : σ ∈ Γque l'environnement Γinclut le fait qui xa du type σ.
• ⊢peut être lu comme le prouve ou le détermine. Γ ⊢ x : σsignifie que l'environnement Γdétermine qu'il xa un type σ.
• ,est un moyen d' inclure des hypothèses supplémentaires spécifiques dans un environnement Γ.
  Par conséquent, Γ, x : τ ⊢ e : τ'signifie que l'environnement Γ, avec l'hypothèse supplémentaire et prioritaire qui xa le typeτ , prouve qu'il ea le type τ'.

Comme demandé: priorité de l'opérateur, du plus haut au plus bas:

• Infix spécifiques à la langue et les opérateurs mixfix, tels que λ x . e, ∀ α . σet τ → τ', let x = e0 in e1et des espaces pour l' application de la fonction.
• :
• ∈ et ∉
• , (gauche-associatif)
• ⊢
• espace séparant plusieurs propositions (associatif)
• la barre horizontale

Cette syntaxe, bien qu'elle puisse sembler compliquée, est en fait assez simple. L'idée de base vient de la logique formelle: 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. Autrement dit, si vous savez que les expressions supérieures sont vraies, vous pouvez conclure que les expressions inférieures sont également vraies.

Symboles

Une autre chose à garder à l'esprit est que certaines lettres ont des significations traditionnelles; en particulier, Γ représente le «contexte» dans lequel vous vous trouvez, c'est-à-dire les types d'autres choses que vous avez vues. Donc, quelque chose comme Γ ⊢ ..."l'expression" ...lorsque vous connaissez les types de chaque expression Γ.

Le ⊢symbole signifie essentiellement que vous pouvez prouver quelque chose. Il en Γ ⊢ ...va de même pour une déclaration disant: «Je peux prouver ...dans un contexte Γ. Ces déclarations sont également appelées jugements de type.

Une autre chose à garder à l'esprit: en mathématiques, tout comme ML et Scala, x : σsignifie que le xtype a σ. Vous pouvez le lire comme celui de Haskell x :: σ.

Signification de chaque règle

Donc, sachant cela, la première expression devient facile à comprendre: si nous savons que x : σ ∈ Γ(c'est-à-dire, xa un certain type σdans un certain contexte Γ), alors nous savons que Γ ⊢ x : σ(c'est-à-dire, dans Γ, xa un type σ). Donc vraiment, cela ne vous dit rien de super intéressant; il vous indique simplement comment utiliser votre contexte.

Les autres règles sont également simples. Par exemple, prenez [App]. Cette règle a deux conditions: e₀est une fonction d'un certain type τà un certain type τ'et e₁est une valeur de type τ. Maintenant , vous savez quel type vous obtiendrez en appliquant e₀à e₁! Espérons que ce ne soit pas une surprise :).

La règle suivante a une nouvelle syntaxe. En particulier, Γ, x : τsignifie simplement le contexte constitué Γet le jugement x : τ. Donc, si nous savons que la variable xa un type de τet que l'expression ea un type τ', nous connaissons également le type d'une fonction qui prend xet renvoie e. Cela nous dit simplement quoi faire si nous avons compris quel type de fonction prend et quel type elle renvoie, donc cela ne devrait pas être surprenant non plus.

La suivante vous indique simplement comment gérer les letinstructions. Si vous savez qu'une expression e₁a un type τtant qu'elle xa un type σ, alors une letexpression qui se lie localement xà une valeur de type σaura e₁un type τ. Vraiment, cela vous indique simplement qu'une instruction let vous permet essentiellement d'étendre le contexte avec une nouvelle liaison, ce qui est exactement ce qui letfait!

La [Inst]règle traite du sous-typage. Il dit que si vous avez une valeur de type σ'et qu'il s'agit d'un sous-type de σ( ⊑représente une relation d'ordre partiel), alors cette expression est également de type σ.

La dernière règle concerne la généralisation des types. Un petit côté: une variable libre est une variable qui n'est pas introduite par une instruction let ou lambda dans une expression; cette expression dépend maintenant de la valeur de la variable libre de son contexte. La règle dit que s'il y a 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 vous connaissez le type e : σaura ce type pour n'importe quelle valeur de α.

Comment utiliser les règles

Alors, maintenant que vous comprenez les symboles, que faites-vous de ces règles? Eh bien, vous pouvez utiliser ces règles pour déterminer le type de différentes valeurs. Pour ce faire, examinez votre expression (par exemple f x y) et trouvez une règle dont la conclusion (la partie inférieure) correspond à votre affirmation. Appelons la chose que vous essayez de trouver votre "objectif". Dans ce cas, vous examineriez la règle qui se termine par e₀ e₁. Lorsque vous avez trouvé cela, vous devez maintenant trouver des règles prouvant tout au-dessus de la ligne de cette règle. Ces éléments correspondent généralement aux types de sous-expressions, vous recourez donc essentiellement à certaines parties de l'expression. Vous faites cela jusqu'à ce que vous ayez terminé votre arbre de preuve, ce qui vous donne une preuve du type de votre expression.

Donc, toutes ces règles ne spécifient exactement - et dans le détail mathématique habituel: P - comment comprendre les types d'expressions.

Maintenant, cela devrait vous sembler familier si vous avez déjà utilisé Prolog - vous calculez essentiellement l'arbre de preuve comme un interpréteur Prolog humain. Il y a une raison pour laquelle Prolog est appelé "programmation logique"! Ceci est également important car la première façon dont j'ai été présenté à l'algorithme d'inférence HM a été de l'implémenter dans Prolog. C'est en fait étonnamment simple et rend clair ce qui se passe. Vous devriez certainement l'essayer.

Remarque: J'ai probablement fait des erreurs dans cette explication et j'aimerais que quelqu'un les signale. En fait, je couvrirai cela en classe dans quelques semaines, alors je serai plus confiant alors: P.

si quelqu'un pouvait au moins me dire par où commencer pour chercher à comprendre ce que cette mer de symboles signifie

Voir « Fondements pratiques des langages de programmation », chapitres 2 et 3, sur le style de la logique par les jugements et les dérivations. L'intégralité du livre est désormais disponible sur Amazon.

Chapitre 2

Définitions inductives

Les définitions inductives sont un outil indispensable dans l'étude des langages de programmation. Dans ce chapitre, nous développerons le cadre de base des définitions inductives et donnerons quelques exemples de leur utilisation. Une définition inductive consiste en un ensemble de règles permettant de dériver des jugements , ou assertions , de diverses formes. Les jugements sont des déclarations sur un ou plusieurs objets syntaxiques d'un type spécifié. Les règles précisent les conditions nécessaires et suffisantes pour la validité d'un jugement et déterminent donc pleinement sa signification.

2.1 Jugements

Nous commençons par la notion de jugement , ou assertion sur un objet syntaxique. Nous utiliserons de nombreuses formes de jugement, y compris des exemples tels que ceux-ci:

• n nat - n est un nombre naturel
• n = n1 + n2 - n est la somme de n1 et n2
• τ type - τ est un type
• e : τ - l'expression e a le type τ
• e ⇓ v - l'expression e a une valeur v

Un jugement déclare qu'un ou plusieurs objets syntaxiques ont une propriété ou sont en relation les uns avec les autres. La propriété ou la relation elle-même est appelée une forme de jugement , et le jugement selon lequel un objet ou des objets ont cette propriété ou se tiennent dans cette relation serait une instance de cette forme de jugement. Une forme de jugement est également appelée prédicat , et les objets constituant une instance en sont les sujets . Nous écrivons un J pour le jugement affirmant que J détient un . Quand il n'est pas important d'insister sur le sujet de l'arrêt, (le texte est coupé ici)

Comment puis-je comprendre les règles Hindley-Milner?

Hindley-Milner est un ensemble de règles sous forme de calcul séquentiel (pas de déduction naturelle) qui démontre que nous pouvons déduire le type (le plus général) d'un programme de la construction du programme sans déclarations de type explicites.

Les symboles et la notation

Tout d'abord, expliquons les symboles et discutons de la priorité des opérateurs

• 𝑥 est un identifiant (de manière informelle, un nom de variable).
• : signifie est un type de (de manière informelle, une instance de ou "is-a").
• 𝜎 (sigma) est une expression qui est soit une variable soit une fonction.
• ainsi 𝑥: 𝜎 se lit " 𝑥 is-a 𝜎 "
• ∈ signifie "est un élément de"
• 𝚪 (Gamma) est un environnement.
• ⊦ (le signe d'assertion) signifie affirme (ou prouve, mais "affirme" contextuellement se lit mieux.)
• 𝚪 ⊦ 𝑥 : 𝜎 se lit donc "𝚪 affirme que 𝑥, est-a 𝜎 "
• 𝑒 est une instance (élément) réelle de type 𝜎 .
• 𝜏 (tau) est un type: basique, variable ( 𝛼 ), fonctionnel 𝜏 → 𝜏 ' ou produit 𝜏 × 𝜏' (le produit n'est pas utilisé ici)
• 𝜏 → 𝜏 ' est un type fonctionnel où 𝜏 et 𝜏' sont des types potentiellement différents.

• 𝜆𝑥.𝑒 signifie que 𝜆 (lambda) est une fonction anonyme qui prend un argument, 𝑥 , et renvoie une expression, 𝑒 .

• soit 𝑥 = 𝑒₀ dans 𝑒₁ signifie dans l'expression, 𝑒₁ , remplacez 𝑒₀ partout où 𝑥 apparaît.

• ⊑ signifie que l'élément précédent est un sous-type (informellement - sous-classe) de ce dernier élément.

• 𝛼 est une variable de type.
• ∀ 𝛼.𝜎 est un type, ∀ (pour tous) les variables d'argument, 𝛼 , renvoyant l' expression 𝜎
• ∉ libre (𝚪) ne signifie pas un élément des variables de type libre de 𝚪 définies dans le contexte externe. (Les variables liées sont substituables.)

Tout au-dessus de la ligne est la prémisse, tout en dessous est la conclusion ( Per Martin-Löf )

Priorité, par exemple

J'ai pris certains des exemples les plus complexes des règles et inséré des parenthèses redondantes qui montrent la priorité:

• 𝑥: 𝜎 ∈ 𝚪 pourrait s'écrire (𝑥: 𝜎) ∈ 𝚪

• 𝚪 ⊦ 𝑥 : 𝜎 pourrait s'écrire 𝚪 ⊦ ( 𝑥 : 𝜎 )

• 𝚪 ⊦ let 𝑥 = 𝑒₀ in 𝑒₁ : 𝜏 est équivalent 𝚪 ⊦ (( let ( 𝑥 = 𝑒₀ ) in 𝑒₁ ): 𝜏 )

• 𝚪 ⊦ 𝜆𝑥.𝑒 : 𝜏 → 𝜏 ' est équivalent 𝚪 ⊦ (( 𝜆𝑥.𝑒 ): ( 𝜏 → 𝜏' ))

Ensuite, de grands espaces séparant les déclarations d'assertion et d'autres conditions préalables indiquent un ensemble de telles conditions préalables, et enfin la ligne horizontale séparant le principe de la conclusion fait apparaître la fin de l'ordre de priorité.

Les règles

Ce qui suit ici sont des interprétations anglaises des règles, chacune suivie d'un retraitement lâche et d'une explication.

Variable

Étant donné que 𝑥 est un type de 𝜎 (sigma), un élément de 𝚪 (Gamma),
concluez que 𝚪 affirme que 𝑥 est un 𝜎.

Autrement dit, dans 𝚪, nous savons que 𝑥 est de type 𝜎 parce que 𝑥 est de type 𝜎 dans 𝚪.

Il s'agit essentiellement d'une tautologie. Un nom d'identifiant est une variable ou une fonction.

Application de fonction

Étant donné que 𝚪 affirme 𝑒₀ est un type fonctionnel et 𝚪 affirme que 𝑒₁ est un 𝜏
conclure 𝚪 affirme que l'application de la fonction 𝑒₀ à 𝑒₁ est un type 𝜏 '

Pour reformuler la règle, nous savons que l'application de fonction retourne le type 𝜏 'car la fonction a le type 𝜏 → 𝜏' et obtient un argument de type 𝜏.

Cela signifie que si nous savons qu'une fonction renvoie un type et que nous l'appliquons à un argument, le résultat sera une instance du type que nous savons qu'elle renvoie.

Abstraction de fonction

Étant donné que 𝚪 et 𝑥 de type 𝜏 affirme 𝑒 est un type, 𝜏 '
conclure 𝚪 affirme une fonction anonyme, 𝜆 de 𝑥 renvoyant une expression, 𝑒 est de type 𝜏 → 𝜏'.

Encore une fois, quand nous voyons une fonction qui prend 𝑥 et renvoie une expression 𝑒, nous savons qu'elle est de type 𝜏 → 𝜏 'parce que 𝑥 (a 𝜏) affirme que 𝑒 est un 𝜏'.

Si nous savons que 𝑥 est de type 𝜏 et donc qu'une expression 𝑒 est de type 𝜏 ', alors une fonction de 𝑥 renvoyant l'expression 𝑒 est de type 𝜏 → 𝜏'.

Soit déclaration de variable

Étant donné 𝚪 assert 𝑒₀, de type 𝜎, et 𝚪 et 𝑥, de type 𝜎, les assert 𝑒₁ de type 𝜏
concluent 𝚪 affirme let𝑥 = 𝑒₀ in𝑒₁ de type 𝜏

En gros, 𝑥 est lié à 𝑒₀ dans 𝑒₁ (a 𝜏) parce que 𝑒₀ est un 𝜎, et 𝑥 est un 𝜎 qui affirme que 𝑒₁ est un 𝜏.

Cela signifie que si nous avons une expression 𝑒₀ qui est un 𝜎 (étant une variable ou une fonction), et un nom, 𝑥, également un 𝜎, et une expression 𝑒₁ de type 𝜏, alors nous pouvons substituer 𝑒₀ à 𝑥 partout où il apparaît à l'intérieur de 𝑒₁.

Instanciation

Étant donné que 𝚪 affirme 𝑒 de type 𝜎 'et 𝜎' est un sous-type de 𝜎
concluez 𝚪 affirme que 𝑒 est de type 𝜎

Une expression, 𝑒 est du type parent 𝜎 car l'expression 𝑒 est du sous-type 𝜎 ', et 𝜎 est le type parent de 𝜎'.

Si une instance est d'un type qui est un sous-type d'un autre type, alors c'est également une instance de ce super-type - le type plus général.

Généralisation

Étant donné que 𝚪 affirme que 𝑒 est un 𝜎 et que 𝛼 n'est pas un élément des variables libres de 𝚪,
concluez que 𝚪 affirme 𝑒, tapez pour toutes les expressions d'argument 𝛼 renvoyant une expression 𝜎

Donc en général, 𝑒 est tapé 𝜎 pour toutes les variables d'argument (𝛼) retournant 𝜎, car nous savons que 𝑒 est un 𝜎 et 𝛼 n'est pas une variable libre.

Cela signifie que nous pouvons généraliser un programme pour accepter tous les types d'arguments qui ne sont pas déjà liés dans la portée contenante (variables qui ne sont pas non locales). Ces variables liées sont substituables.

Mettre tous ensemble

Compte tenu de certaines hypothèses (comme l'absence de variables libres / non définies, un environnement connu), nous connaissons les types de:

• éléments atomiques de nos programmes (Variable),
• valeurs renvoyées par les fonctions (Function Application),
• constructions fonctionnelles (Function Abstraction),
• let bindings (Let Variable Declarations),
• types d'instances parent (Instanciation), et
• toutes les expressions (généralisation).

Conclusion

Ces règles combinées nous permettent de prouver le type le plus général d'un programme affirmé, sans exiger d'annotations de type.

La notation vient de la déduction naturelle .

Le symbole is est appelé tourniquet .

Les 6 règles sont très simples.

Var La règle est plutôt banale - elle dit que si le type pour l'identifiant est déjà présent dans votre environnement de type, alors pour déduire le type, vous le prenez simplement de l'environnement tel quel.

AppLa règle dit que si vous avez deux identifiants e0et e1que vous pouvez déduire leurs types, vous pouvez déduire le type d'application e0 e1. La règle se lit comme ceci si vous le savez e0 :: t0 -> t1et e1 :: t0(le même t0!), Alors l'application est bien typée et le type l'est t1.

Abset Letsont des règles pour déduire des types d'abstraction lambda et d'admission.

Inst La règle dit que vous pouvez remplacer un type par un type moins général.

Il y a deux façons de penser à e: σ. L'un est "l'expression e a le type σ", l'autre est "la paire ordonnée de l'expression e et du type σ".

Voir Γ comme la connaissance des types d'expressions, implémentée comme un ensemble de paires d'expression et de type, e: σ.

Le tourniquet ⊢ signifie qu'à partir des connaissances de gauche, nous pouvons déduire ce qui se trouve à droite.

On peut donc lire la première règle [Var]:
Si notre connaissance Γ contient le couple e: σ, alors on peut déduire de Γ que e a le type σ.

La deuxième règle [App] peut être lue:
Si nous de Γ pouvons déduire que e_0 a le type τ → τ ', et nous de Γ pouvons déduire que e_1 a le type τ, alors nous de Γ pouvons déduire que e_0 e_1 a le tapez τ '.

Il est courant d'écrire Γ, e: σ au lieu de Γ ∪ {e: σ}.

La troisième règle [Abs] peut donc être lue:
Si nous de Γ étendu avec x: τ pouvons déduire que e a le type τ ', alors nous de Γ pouvons déduire que λx.e a le type τ → τ'.

La quatrième règle [Let] est laissée comme exercice. :-)

La cinquième règle [Inst] peut être lue:
Si nous de Γ pouvons déduire que e a le type σ ', et σ' est un sous-type de σ, alors nous de Γ pouvons déduire que e a le type σ.

La sixième et dernière règle [Gen] peut être lue:
Si nous de Γ pouvons déduire que e a le type σ, et α n'est une variable de type libre dans aucun des types de Γ, alors nous de Γ pouvons déduire que e a le type ∀α σ.