Hindley-Milner est un système de type découvert indépendamment par Roger Hindley (qui était à la recherche à la logique) et, plus tard, par Robin Milner (qui était à la recherche à des langages de programmation). Les avantages de Hindley-Milner sont
Il prend en charge polymorphes fonctions; par exemple, une fonction qui peut vous donner la longueur de la liste indépendante du type des éléments, ou une fonction binaire de l'arbre de recherche indépendant du type de clés stockées dans l'arbre.
-
Parfois, une fonction ou d'une valeur de plus d'un type, comme dans l'exemple de la longueur de la fonction: il peut être "liste d'entiers integer", "liste de chaînes de caractères en entier", "liste de paires d'entiers", et ainsi de suite. Dans ce cas, un signal parti de la Hindley-Milner système est que chaque bien tapé terme unique de "meilleur" de type, qui est appelé le type principal. Le principal type de liste de la longueur de la fonction est "pour n'importe quel a, en fonction de la liste d' a entier". Ici, a est un soi-disant "paramètre de type," ce qui est explicite dans le lambda calcul , mais implicite dans la plupart des langages de programmation. L'utilisation de paramètres de type explique pourquoi Hindley-Milner est un système qui met en œuvre paramétrique polymorphisme. (Si vous écrivez une définition de la longueur de la fonction en ML, vous pouvez voir le type de paramètre ainsi:
fun 'a length [] = 0
| 'a length (x::xs) = 1 + length xs
Si un terme a une Hindley-Milner type, puis le type principal peut être déduit sans exiger n'importe quel type de déclarations ou d'autres annotations par le programmeur. (C'est une arme à double tranchant, car tout le monde peut en témoigner, qui n'a jamais été traité une grande partie de la ML code sans annotations.)
Hindley-Milner est la base pour le système de type de presque tous les statiquement typé langage fonctionnel. Ces langues dans l'usage commun comprennent
Toutes ces langues ont étendu Hindley-Milner; Haskell, Propre et Objective Caml faire dans ambitieuse et inédite. (Les Extensions sont nécessaires pour traiter mutable variables, depuis la base de Hindley-Milner peut être subverti en utilisant, par exemple, une mutable cellule de la tenue d'une liste de valeurs de type non spécifié. De tels problèmes sont traités par une extension appelée la valeur de restriction.)
De nombreuses autres langues mineures et des outils basés sur des langages fonctionnels typés utilisation de Hindley-Milner.
Hindley-Milner est la restriction de F, ce qui permet plus de types, mais qui nécessite des annotations par le programmeur.
