Qu'est-ce que Hindley-Milner?

Question

Je rencontrais ce terme Hindley-Milner , et je ne suis pas sûr de saisir ce que cela signifie.

J'ai lu les messages suivants:

• Steve Yegge - Langues Dynamic Strike Back
• Steve Yegge - Le Pinocchio problème
• Daniel Spiewak - Qu'est-ce que est Hindley-Milner? (Et pourquoi est-il cool?)

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

Qu'est-ce?
Quelles sont les langues et les outils mettre en œuvre ou l'utiliser?
Pourriez-vous s'il vous plaît donner une réponse concise?

Answer 1

Hindley-Milner est un système de type découvert indépendamment par Roger Hindley (qui regardait la logique) et plus tard par Robin Milner (qui regardait les 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 indépendante liste du type des éléments, ou une fonction fait un indépendant de recherche binaire arbre du type de clés stockées dans l'arbre.

• Parfois, une fonction ou valeur peut avoir plus d'un type , comme dans l'exemple de la fonction de la longueur: il peut être « liste des entiers à un entier », « liste de chaînes à entier », « liste de paires vers entier », et ainsi de suite. Dans ce cas, un avantage de signal du système Hindley-Milner est que chaque terme bien typé a un type "meilleur" unique , qui est appelé type principal . Le type principal de la fonction liste de longueur est « pour toute a, fonction à partir de la liste des a à l'entier ». Ici a est un soi-disant "paramètre de type", qui est explicite dans le calcul lambda et implicite dans la plupart des langages de programmation . L'utilisation de paramètres de type explique pourquoi Hindley-Milner est un système qui implémente paramétrique polymorphisme . (Si vous écrivez une définition de la fonction de la longueur en 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, puis le principal type peut être déduit sans exiger de déclarations de type ou d'autres annotations par le programmeur. (Ceci est une bénédiction mitigée, comme tout le monde peut en témoigner qui n'a jamais été traité un grand morceau de code ML sans annotations.)

Hindley-Milner est la base du système de type de presque tous statiquement langage fonctionnel typé. Ces langues d'usage courant comprennent

• La famille ML ( Standard ML et Objectif Caml)
• Haskell
• Clean

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

Beaucoup d'autres langues mineures et des outils basés sur les langages fonctionnels typés utilisent Hindley-Milner.

Hindley-Milner est une restriction de de, ce qui permet plusieurs types mais nécessite annotations par le programmeur .

Answer 2

Vous pouvez être en mesure de trouver les documents originaux en utilisant Google Scholar ou CiteSeer - ou votre bibliothèque universitaire locale. Le premier est assez vieux que vous pourriez avoir à trouver des exemplaires reliés de la revue, je ne pouvais pas trouver en ligne. Le lien que j'ai trouvé pour l'autre était cassé, mais il pourrait y avoir d'autres. Vous serez certainement en mesure de trouver des documents qui citent ces derniers.

Hindley, Roger J, Le système de type principal d'un objet dans la logique combinatoire , Transactions de l'American Mathematical Society, 1969.

Milner, Robin, Une théorie de type Polymorphisme , Journal of Computer Sciences et système, 1978.

Answer 3

simple mise en œuvre de l'inférence de type Hindley-Milner en C #:

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

Notez que la mise en œuvre est de l'ordre de seulement 270 ou si des lignes de C # (pour l'algorithme W approprié et les quelques structures de données pour le soutenir, 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 aussi Brian McKenna mise en œuvre JavaScript sur bitbucket, ce qui contribue également à obtenir Démarrage rapide (travaillé pour moi).

'HTH,