implémentation de l'inférence de type

Je vois ici des discussions intéressantes sur le typage statique et dynamique. Je préfère généralement le typage statique, en raison de la vérification du type de compilation, du code mieux documenté, etc. Cependant, je suis d'accord pour dire qu'ils encombrent le code si cela est fait comme Java, par exemple.

Je suis donc sur le point de commencer à créer mon propre langage de style fonctionnel, et l'inférence de type est l'une des choses que je souhaite implémenter. Je comprends que c'est un gros sujet, et je n'essaie pas de créer quelque chose qui n'a pas été fait auparavant, juste des inférences de base ...

Des conseils sur ce qu'il faut lire qui m'aidera avec cela? De préférence quelque chose de plus pragmatique / pratique par opposition à des textes de théorie des catégories / théorie des types plus théoriques. S'il y a un texte de discussion sur l'implémentation, avec des structures de données / algorithmes, ce serait tout simplement charmant.

J'ai trouvé les ressources suivantes utiles pour comprendre l'inférence de type, par ordre de difficulté croissante:

1. Le chapitre 30 (Type Inference) du livre disponible gratuitement PLAI , Langages de programmation: application et interprétation , esquisse l'inférence de type basée sur l'unification.
2. Le cours d'été Interpréter les types comme des valeurs abstraites présente des évaluateurs élégants, des vérificateurs de types, des reconstructeurs de types et des inférenceurs utilisant Haskell comme métalangage.
3. Chapitre 7 (Types) du livre EOPL , Essentials of Programming Languages .
4. Chapitre 22 (Reconstruction de types) du livre TAPL , Types and Programming Languages , et les implémentations OCaml correspondantes recon et fullrecon .
5. Chapitre 13 (Reconstruction de type) du nouveau livre DCPL , Design Concepts in Programming Languages .
6. Sélection d'articles académiques .
7. TypeInference du compilateur de fermeture est un exemple de l'approche d'analyse de flux de données pour l'inférence de type, qui est mieux adaptée aux langages dynamiques que l'approche Hindler Milner.

Cependant, comme la meilleure façon d'apprendre est de faire, je suggère fortement d'implémenter l'inférence de type pour un langage fonctionnel de jouet en travaillant à travers une tâche à domicile d'un cours de langages de programmation.

Je recommande ces deux devoirs accessibles en ML, que vous pouvez tous deux terminer en moins d'une journée:

1. Interpréteur PCF ( une solution ) pour se réchauffer.
2. Inférence de type PCF ( une solution ) pour implémenter l'algorithme W pour l'inférence de type Hindley-Milner.

Ces devoirs proviennent d'un cours plus avancé:

1. Implémentation de MiniML

2. Types polymorphes, existentiels et récursifs (PDF)

3. Vérification de type bidirectionnelle (PDF)

4. Sous-typage et objets (PDF)

Il est malheureux qu'une grande partie de la littérature sur le sujet soit très dense. Moi aussi j'étais à ta place. J'ai eu ma première introduction au sujet dans Langages de programmation: applications et interprétation

http://www.plai.org/

Je vais essayer de résumer l'idée abstraite suivie de détails que je n'ai pas trouvés immédiatement évidents. Premièrement, l'inférence de type peut être pensée pour générer puis résoudre des contraintes. Pour générer des contraintes, vous parcourez l'arborescence de syntaxe et générez une ou plusieurs contraintes sur chaque nœud. Par exemple, si le nœud est un +opérateur, les opérandes et les résultats doivent tous être des nombres. Un nœud qui applique une fonction a le même type que le résultat de la fonction, et ainsi de suite.

Pour un langage sans let, vous pouvez résoudre aveuglément les contraintes ci-dessus par substitution. Par exemple:

(if (= 1 2) 
    1 
    2)

ici, nous pouvons dire que la condition de l'instruction if doit être booléenne, et que le type de l'instruction if est le même que le type de ses clauses thenand else. Puisque nous connaissons 1et 2sommes des nombres, par substitution, nous savons que l' ifénoncé est un nombre.

Là où les choses deviennent désagréables, et ce que je n'ai pas pu comprendre pendant un moment, c'est que:

(let ((id (lambda (x) x)))
    (id id))

Ici, nous sommes liés idà une fonction qui renvoie tout ce que vous avez passé, autrement connu sous le nom de fonction d'identité. Le problème est que le type de paramètre de la fonction xest différent à chaque utilisation de id. La seconde idest une fonction de type a -> a, où apeut être n'importe quoi. Le premier est de type (a -> a) -> (a -> a). Ceci est connu sous le nom de let-polymorphisme. La clé est de résoudre les contraintes dans un ordre particulier: commencez par résoudre les contraintes pour la définition de id. Ce sera a -> a. Ensuite, des copies fraîches et séparées du type de idpeuvent être substituées dans les contraintes pour chaque lieu id, par exemple a2 -> a2et a3 -> a3.

Cela n'a pas été facilement expliqué dans les ressources en ligne. Ils mentionneront l'algorithme W ou M, mais pas comment ils fonctionnent en termes de résolution des contraintes, ou pourquoi il ne barf sur let-polymorphisme: chacun de ces algorithmes applique un ordre sur la résolution des contraintes.

J'ai trouvé cette ressource extrêmement utile pour lier les algorithmes W, M et le concept général de génération et de résolution de contraintes. C'est un peu dense, mais meilleur que beaucoup:

http://www.cs.uu.nl/research/techreps/repo/CS-2002/2002-031.pdf

La plupart des autres articles sont également intéressants:

http://people.cs.uu.nl/bastiaan/papers.html

J'espère que cela aidera à clarifier un monde quelque peu trouble.

Outre Hindley Milner pour les langages fonctionnels, une autre approche populaire de l'inférence de type pour le langage dynamique est abstract interpretation.

L'idée de l'interprétation abstraite est d'écrire un interpréteur spécial pour le langage, au lieu de garder un environnement de valeurs concrètes (1, false, fermeture), cela fonctionne sur des valeurs abstraites, aka types (int, bool, etc.). Puisqu'il interprète le programme sur des valeurs abstraites, c'est pourquoi on l'appelle interprétation abstraite.

Pysonar2 est une implémentation élégante d'interprétation abstraite pour Python. Il est utilisé par Google pour analyser les projets Python. Fondamentalement, il utilise visitor patternpour envoyer l'appel d'évaluation au nœud AST concerné. La fonction visiteur transform accepte le contextdans lequel le nœud actuel sera évalué et renvoie le type de nœud actuel.

Types et langages de programmation par Benjamin C. Pierce

Lambda l'ultime, à partir d' ici .