Recherche sur l'inférence de type basée sur le site d'appel?

9

J'essaie d'en savoir plus sur les systèmes de vérification de type de programme complet et d'inférence de type qui utilisent les informations des sites d'appel de fonction pour calculer les informations de type (en plus de l'approche standard d'utilisation du corps de fonction). Par exemple, un tel algorithme pourrait utiliser un appel de fonction comme foo(1)pour déduire que la fonction dans fooprend des arguments entiers. Évidemment, cela compliquerait beaucoup l'inférence et rendrait le chèque non modulaire.

Quoi qu'il en soit, je n'ai pas eu beaucoup de chance pour trouver des recherches sur cette approche, probablement parce que je ne connais pas la bonne terminologie pour décrire ce dont je parle. Des pointeurs?

Derek Thurn
la source
Ce que vous décrivez contient des indices d'inférence de type bidirectionnel, sauf erreur de ma part. Décrire ce que vous essayez de faire peut cependant clarifier.
Dominic Mulligan
Le demandez-vous parce que vous cherchez un moyen de spécialiser les fonctions polymorphes?
nponeccop
J'essaie surtout d'en savoir plus sur les systèmes de types vraiment, et oui, je pensais surtout à la façon de gérer les fonctions polymorphes (et les appels de méthode dans les langages OO, la même chose). J'essaie d'identifier les bons termes pour cela afin que je puisse le lire.
Derek Thurn

Réponses:

11

Pour ce faire, presque tous les systèmes avec inférence de type utilisent des informations sur le site d'appel. Les exemples incluent Standard ML, OCaml, F # et Haskell. De nombreux autres langages utilisent les informations du site d'appel pour déduire l'instanciation des paramètres de type, tels que Java, C #, Scala et Typed Racket. Cela s'appelle souvent "Inférence de type local".

Je décrirais simplement ce que vous recherchez comme "Type Inference", et vous devriez probablement commencer par rechercher ce qui est communément appelé le système "Hindley-Milner". La page Wikipedia donne une introduction raisonnable et des pointeurs vers les articles originaux.

Le point de départ pour l'inférence de type locale est le document original de Pierce et Turner, mieux lu dans la version TOPLAS 2000 ( ACM , PDF ).

Sam Tobin-Hochstadt
la source
Le document de Pierce et Turner était très instructif, merci. Connaissez-vous une implémentation minimale de l'algorithme décrit dans le code? Je pense que ce serait très intéressant de regarder aussi, s'il existe.
Derek Thurn
Je ne connais aucune implémentation minimale. Il y en a un dans Typed Racket et un dans Scala, mais les deux implémentent des algorithmes beaucoup plus compliqués.
Sam Tobin-Hochstadt
0

Vous pouvez jeter un oeil aux systèmes de types pour les types d'intersection qui peuvent vous donner quelque chose comme ça a :: Int -> Int | Bool -> Bool, donc vous savez que deux spécialisations Intet Boolsuffisent, ou utiliser une inférence de type habituelle pour déduire la plupart des types généraux suivie d'une analyse de flux de contrôle pour collecter les données réelles arguments de type. En fait, il existe des approches hybrides (CFA exprimé comme un système de type et vice versa).

Des travaux de recherche sur l'inférence des types les moins généraux au lieu de la plupart des types généraux peuvent exister, mais je ne les connais pas.

En ce qui concerne les techniques pour implémenter le polymorphisme, deux solutions existent: 1) spécialisation (pensez aux modèles C ++) 2) hypothèse de représentation uniforme (pensez aux collections de style C avec void *).

Pour 2, vous n'avez pas besoin du type du site d'appel pendant la vérification de type et pouvez prendre en charge plus facilement la compilation séparée.

Notez que nous parlons ici de polymorphisme paramétrique, et les appels de méthode virtuelle OO sont une chose complètement différente appelée polymorphisme de sous-type. Notez que les modèles C ++ prennent en charge à la fois quelque chose comme le polymorphisme paramétrique et le typage canard, qui est encore une autre forme de polymorphisme.

nponeccop
la source
1
"Les appels de méthode virtuelle OO sont une chose complètement différente appelée polymorphisme ad hoc" Le polymorphisme ad hoc est un autre nom pour la surcharge. Vous semblez le confondre avec le polymorphisme de sous-type.
Radu GRIGore
Mais les sous-classes ne sont pas nécessairement des sous-types, n'est-ce pas? Par exemple, pour les sous-types, LSP est censé tenir.
nponeccop
1
C'est vrai, mais à côté du point. "Polymorphisme de sous-type" est le terme standard. Voir en.wikipedia.org/wiki/Subtype_polymorphism pour plus de détails.
Radu GRIGore