Qu'est-ce que Hindley-Milner?

J'ai rencontré ce terme Hindley-Milner , et je ne suis pas sûr de comprendre ce que cela signifie.

J'ai lu les articles suivants:

• Steve Yegge - Les langues dynamiques contre-attaquent
• Steve Yegge - Le problème de Pinocchio
• Daniel Spiewak - Qu'est - ce que Hindley-Milner? (et pourquoi est-ce cool?)

Mais il n'y a pas d'entrée unique pour ce terme dans wikipedia où m'offre généralement une explication concise.
^{Remarque - un a maintenant été ajouté}

Qu'Est-ce que c'est?
Quels langages et outils l'implémentent ou l'utilisent?
Souhaitez-vous s'il vous plaît offrir une réponse concise?

Hindley-Milner est un système de type découvert indépendamment par Roger Hindley (qui s'intéressait à la logique) et plus tard par Robin Milner (qui s'intéressait aux langages de programmation). Les avantages de Hindley-Milner sont

• Il prend en charge les fonctions polymorphes ; par exemple, une fonction qui peut vous donner la longueur de la liste indépendamment du type des éléments, ou une fonction effectue une recherche dans l'arborescence binaire indépendamment du type de clés stockées dans l'arborescence.

• Parfois, une fonction ou une valeur peut avoir plus d'un type , comme dans l'exemple de la fonction length: il peut s'agir de "liste d'entiers en entier", "liste de chaînes en entier", "liste de paires en entier", etc. sur. Dans ce cas, un avantage de signal du système Hindley-Milner est que chaque terme bien typé a un type unique "meilleur" , qui est appelé le type principal . Le type principal de la fonction de longueur de liste est "pour tout a, fonction de liste de aà entier". Voici aun soi-disant «paramètre de type», qui est explicite dans le calcul lambda mais implicite dans la plupart des langages de programmation .polymorphisme paramétrique . (Si vous écrivez une définition de la fonction de longueur dans ML, vous pouvez voir le paramètre de type ainsi:

   fun 'a length []      = 0
     | 'a length (x::xs) = 1 + length xs
  

• Si un terme a un type Hindley-Milner, alors le type principal peut être déduit sans nécessiter de déclaration de type ou d'autres annotations par le programmeur. (C'est une bénédiction mitigée, comme n'importe qui peut en attester qui a déjà été manipulé un gros morceau de code ML sans annotations.)

Hindley-Milner est la base du système de types de presque tous les langages fonctionnels à typage statique. Ces langues d'usage courant comprennent

• La famille ML ( Standard ML et Objective Caml )
• Haskell
• Nettoyer

Toutes ces langues ont étendu Hindley-Milner; Haskell, Clean et Objective Caml le font de manière ambitieuse et inhabituelle. (Les extensions sont nécessaires pour traiter les variables mutables, car Hindley-Milner de base peut être subvertie en utilisant, par exemple, une cellule mutable contenant une liste de valeurs de type non spécifié. Ces problèmes sont traités par une extension appelée restriction de valeur .)

De nombreux autres langages mineurs et outils basés sur des langages fonctionnels typés utilisent Hindley-Milner.

Hindley-Milner est une restriction de System F , qui autorise plus de types mais qui nécessite des annotations de la part du programmeur .

Vous pourrez peut-être trouver les articles originaux en utilisant Google Scholar ou CiteSeer - ou votre bibliothèque universitaire locale. Le premier est assez vieux pour que vous deviez peut-être trouver des exemplaires reliés du journal, je ne l'ai pas trouvé en ligne. Le lien que j'ai trouvé pour l'autre était rompu, mais il y en a peut-être d'autres. Vous pourrez certainement trouver des articles qui les citent.

Hindley, Roger J, Le schéma de type principal d'un objet en logique combinatoire , Transactions of the American Mathematical Society, 1969.

Milner, Robin, Une théorie du polymorphisme de type , Journal of Computer and System Sciences, 1978.

Implémentation d'inférence de type Hindley-Milner simple en C #:

Inférence de type Hindley-Milner sur des expressions S (Lisp-ish), en moins de 650 lignes de C #

Notez que l'implémentation est de l'ordre de seulement 270 lignes de C # (pour l'algorithme W proprement dit et les quelques structures de données pour le supporter, de toute façon).

Extrait d'utilisation:

    // ...

    var syntax =
        new SExpressionSyntax().
        Include
        (
            // Not-quite-Lisp-indeed; just tolen from our host, C#, as-is
            SExpressionSyntax.Token("\\/\\/.*", SExpressionSyntax.Commenting),
            SExpressionSyntax.Token("false", (token, match) => false),
            SExpressionSyntax.Token("true", (token, match) => true),
            SExpressionSyntax.Token("null", (token, match) => null),

            // Integers (unsigned)
            SExpressionSyntax.Token("[0-9]+", (token, match) => int.Parse(match)),

            // String literals
            SExpressionSyntax.Token("\\\"(\\\\\\n|\\\\t|\\\\n|\\\\r|\\\\\\\"|[^\\\"])*\\\"", (token, match) => match.Substring(1, match.Length - 2)),

            // For identifiers...
            SExpressionSyntax.Token("[\\$_A-Za-z][\\$_0-9A-Za-z\\-]*", SExpressionSyntax.NewSymbol),

            // ... and such
            SExpressionSyntax.Token("[\\!\\&\\|\\<\\=\\>\\+\\-\\*\\/\\%\\:]+", SExpressionSyntax.NewSymbol)
        );

    var system = TypeSystem.Default;
    var env = new Dictionary<string, IType>();

    // Classic
    var @bool = system.NewType(typeof(bool).Name);
    var @int = system.NewType(typeof(int).Name);
    var @string = system.NewType(typeof(string).Name);

    // Generic list of some `item' type : List<item>
    var ItemType = system.NewGeneric();
    var ListType = system.NewType("List", new[] { ItemType });

    // Populate the top level typing environment (aka, the language's "builtins")
    env[@bool.Id] = @bool;
    env[@int.Id] = @int;
    env[@string.Id] = @string;
    env[ListType.Id] = env["nil"] = ListType;

    //...

    Action<object> analyze =
        (ast) =>
        {
            var nodes = (Node[])visitSExpr(ast);
            foreach (var node in nodes)
            {
                try
                {
                    Console.WriteLine();
                    Console.WriteLine("{0} : {1}", node.Id, system.Infer(env, node));
                }
                catch (Exception ex)
                {
                    Console.WriteLine(ex.Message);
                }
            }
            Console.WriteLine();
            Console.WriteLine("... Done.");
        };

    // Parse some S-expr (in string representation)
    var source =
        syntax.
        Parse
        (@"
            (
                let
                (
                    // Type inference ""playground""

                    // Classic..                        
                    ( id ( ( x ) => x ) ) // identity

                    ( o ( ( f g ) => ( ( x ) => ( f ( g x ) ) ) ) ) // composition

                    ( factorial ( ( n ) => ( if ( > n 0 ) ( * n ( factorial ( - n 1 ) ) ) 1 ) ) )

                    // More interesting..
                    ( fmap (
                        ( f l ) =>
                        ( if ( empty l )
                            ( : ( f ( head l ) ) ( fmap f ( tail l ) ) )
                            nil
                        )
                    ) )

                    // your own...
                )
                ( )
            )
        ");

    // Visit the parsed S-expr, turn it into a more friendly AST for H-M
    // (see Node, et al, above) and infer some types from the latter
    analyze(source);

    // ...

... ce qui donne:

id : Function<`u, `u>

o : Function<Function<`z, `aa>, Function<`y, `z>, Function<`y, `aa>>

factorial : Function<Int32, Int32>

fmap : Function<Function<`au, `ax>, List<`au>, List<`ax>>

... Done.

Voir également l'implémentation JavaScript de Brian McKenna sur bitbucket, qui aide également à démarrer (a fonctionné pour moi).

«HTH,