implémentation d'inférence de type

Question

et bien je vois quelques discussions intéressantes ici sur la statique vs dynamique de frappe Je préfère généralement le typage statique, en raison de compiler une vérification de type, de mieux documenter le code,etc. Cependant je suis d'accord qu'ils n'encombrent le code si elle est effectuée de la façon dont Java est-il, par exemple.

donc, Im sur le point de commencer la construction d'une langue de mon propre et l'inférence de type est l'une des choses que je veux mettre en œuvre, dans un style fonctionnel de la langue... je ne comprends que c'est un grand sujet, et je ne suis pas essayer de créer quelque chose qui n'a pas été fait avant, juste de base de l'inférence...

tous les pointeurs sur quoi lire jusqu'qui va m'aider avec cela? de préférence quelque chose de plus pragmatique et pratique que de s'opposer à la plus théorique de la catégorie théorie/théorie des types de textes. Si il y a une mise en discussion du texte ici, avec des structures de données/algorithmes, qui serait tout simplement être belle

très apprécié

Answer 1

J'ai trouvé les ressources suivantes utiles pour la compréhension de l'inférence de type, dans l'ordre de difficulté croissante:

1. Chapitre 30 (Inférence de Type) de l'librement disponible livre PLAI, Langages de Programmation: Application et de l'Interprétation, d'esquisses, de l'unification basée sur l'inférence de type.
2. Le cours d'été de l'Interprétation de types de valeurs abstraites présente élégante évaluateurs, type de pions, de type reconstructors et inferencers à l'aide de Haskell comme un métalangage.
3. Le chapitre 7 (Types) de l'ouvrage EOPL, l'essentiel de Langages de Programmation.
4. Chapitre 22 (Type de Reconstruction) de l'ouvrage TAPL, les Types et les Langages de Programmation, et le correspondant de OCaml implémentations recon et fullrecon.
5. Chapitre 13 (Type de Reconstruction) de la nouvelle livre DCPL, des Concepts de Design dans les Langages de Programmation.
6. Sélection de documents académiques.
7. Fermeture du compilateur TypeInference est un exemple de flux de données, méthode d'analyse pour l'inférence de type, qui est mieux adaptée à la dynamique des langues que l'Hindler Milner approche.

Cependant, le meilleur moyen d'apprendre est de le faire, je vous suggère fortement de la mise en œuvre de l'inférence de type pour un jouet fonctionnelle de la langue par le biais d'un devoir à la maison de l'un des langages de programmation cours.

Je recommande ces deux accessibles devoirs en ML, vous pouvez à la fois complète en moins d'une journée:

1. PCF Interprète (une solution) pour se réchauffer.
2. Le PCF, l'Inférence de Type (une solution) pour mettre en œuvre l'algorithme W pour Hindley-Milner, l'inférence de type.

Ces missions sont à partir d'un cours plus avancé:

1. La Mise En Œuvre De MiniML

2. Polymorphes, Existentielle et Types Récursifs (PDF)

3. Bi-Directionnel de Typage (PDF)

4. Le sous-typage et d'Objets (PDF)

Answer 2

Il est regrettable qu'une grande partie de la littérature sur le sujet est très dense. Moi aussi j'ai été dans vos chaussures. J'ai eu ma première introduction aux Langages de Programmation: Applications et Interprétation

http://www.plai.org/

Je vais essayer de résumer l'idée abstraite suivis par les détails que je n'ai pas trouvé tout de suite évident. Tout d'abord, l'inférence de type peut être la pensée de la génération, puis la résolution de contraintes. Pour générer des contraintes, vous recurse par le biais de l'arbre de syntaxe et de générer 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 une langue sans 'laisser', vous pouvez aveuglément résoudre 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 de type boolean, et que le type de l'instruction if est le même que le type de son "puis" et "else" clauses. Depuis que nous savons que 1 et 2 sont des nombres, par substitution, nous savons que l'instruction "if" est un nombre.

Là où les choses deviennent méchants, et que je ne pouvais pas comprendre pour un certain temps, est de traiter avec laisser:

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

Ici, nous avons tenu 'id' pour une fonction qui renvoie ce que vous avez transmis, autrement connu comme la fonction identité. Le problème, c'est le type de paramètre de la fonction " x " est différent sur chaque type d'utilisation de l'id. Le deuxième 'id' est une fonction de a->a, où a peut être rien. La première est de (a->a)->(a->a), de Ce qui est connu comme laissez-le polymorphisme. La clé est de résoudre des contraintes dans un ordre précis: d'abord résoudre les contraintes de la définition de "id". Ce sera un->un. Puis frais, des copies distinctes du type de pièce d'identité peut être substitué dans les contraintes pour chaque lieu de " id " est utilisé, par exemple a2->a2 et a3>a3.

Qui n'a pas été facilement expliqué dans les ressources en ligne. Ils vais vous parler de l'algorithme W ou M, mais pas de la façon dont ils travaillent en terme de résolution de contraintes, ou pourquoi il n'a pas barf sur laissez-polymorphisme: chacun de ces algorithmes d'exécuter une commande sur la résolution de contraintes.

J'ai trouvé cette ressource extrêmement utile pour attacher Algorithme W, M, et le concept général de la contrainte de la génération et de la résolution de l'ensemble. C'est un peu dense, mais mieux que beaucoup d'autres:

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

De nombreux autres documents sont sympa aussi:

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

J'espère que permet de clarifier un peu glauque du monde.

Answer 3

Types et langages de programmation de Benjamin C. Pierce

Answer 4

Lambda the Ultimate, à partir d' ici .

Answer 5

Regarde ça:

http://fsharpcode.blogspot.com/2010/08/hindley-milner-type-inference-sample.html