Was ist Hindley-Milner?

Ich bin auf diesen Begriff Hindley-Milner gestoßen , und ich bin mir nicht sicher, ob ich verstehe, was er bedeutet.

Ich habe folgende Beiträge gelesen:

• Steve Yegge - Dynamische Sprachen schlagen zurück
• Steve Yegge - Das Pinocchio-Problem
• Daniel Spiewak - Was ist Hindley-Milner? (und warum ist es cool?)

Es gibt jedoch keinen einzigen Eintrag für diesen Begriff in Wikipedia, in dem ich normalerweise eine kurze Erklärung bekomme.
^{Hinweis - einer wurde hinzugefügt}

Was ist es?
Welche Sprachen und Tools implementieren oder verwenden es?
Würden Sie bitte eine kurze Antwort geben?

Hindley-Milner ist ein Typensystem, das unabhängig von Roger Hindley (der sich mit Logik befasste) und später von Robin Milner (der sich mit Programmiersprachen befasste) entdeckt wurde. Die Vorteile von Hindley-Milner sind

• Es unterstützt polymorphe Funktionen; Beispiel: Eine Funktion, mit der Sie die Länge der Liste unabhängig vom Typ der Elemente angeben können, oder eine Funktion führt eine Binärbaumsuche unabhängig vom Typ der im Baum gespeicherten Schlüssel durch.

• Manchmal kann eine Funktion oder ein Wert mehr als einen Typ haben , wie im Beispiel der Längenfunktion: Es kann sich um "Liste von Ganzzahlen zu Ganzzahl", "Liste von Zeichenfolgen zu Ganzzahl", "Liste von Paaren zu Ganzzahl" usw. handeln auf. In diesem Fall besteht ein Signalvorteil des Hindley-Milner-Systems darin, dass jeder gut typisierte Term einen eindeutigen "besten" Typ hat , der als Haupttyp bezeichnet wird . Der Haupttyp der Listenlängenfunktion ist "für jede aFunktion von Liste abis Ganzzahl". Hier aist ein sogenannter "Typparameter", der im Lambda-Kalkül explizit, in den meisten Programmiersprachen jedoch implizit enthalten ist .parametrischer Polymorphismus . (Wenn Sie eine Definition der Längenfunktion in ML schreiben, können Sie den Typparameter folgendermaßen sehen:

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

• Wenn ein Begriff einen Hindley-Milner-Typ hat, kann der Haupttyp abgeleitet werden, ohne dass der Programmierer Typdeklarationen oder andere Anmerkungen benötigt. (Dies ist ein gemischter Segen, wie jeder bezeugen kann, der jemals einen großen Teil des ML-Codes ohne Anmerkungen verarbeitet hat.)

Hindley-Milner ist die Basis für das Typensystem fast jeder statisch typisierten Funktionssprache. Solche gebräuchlichen Sprachen umfassen

• Die ML-Familie ( Standard ML und Objective Caml )
• Haskell
• Reinigen

Alle diese Sprachen haben Hindley-Milner erweitert; Haskell, Clean und Objective Caml tun dies auf ehrgeizige und ungewöhnliche Weise. (Erweiterungen sind erforderlich , mit wandelbaren Variablen zu behandeln, da grundlegende Hindley-Milner werden unter Verwendung unterminiert kann zum Beispiel eine veränderbare Zelle eine Liste von Werten einer nicht näher bezeichneten Art. Solche Probleme werden behandelt durch eine Erweiterung namens der Haltewert Einschränkung .)

Viele andere kleinere Sprachen und Tools, die auf typisierten Funktionssprachen basieren, verwenden Hindley-Milner.

Hindley-Milner ist eine Einschränkung von System F , die mehr Typen zulässt, jedoch Anmerkungen des Programmierers erfordert .

Möglicherweise können Sie die Originalarbeiten mit Google Scholar oder CiteSeer oder Ihrer örtlichen Universitätsbibliothek finden. Das erste ist alt genug, dass Sie möglicherweise gebundene Exemplare des Journals finden müssen. Ich konnte es online nicht finden. Die Verbindung, die ich für die andere gefunden habe, war unterbrochen, aber es könnte andere geben. Sie werden sicherlich Papiere finden, die diese zitieren.

Hindley, Roger J, Das Haupttypschema eines Objekts in der kombinatorischen Logik , Transactions of the American Mathematical Society, 1969.

Milner, Robin, Eine Theorie des Typpolymorphismus , Journal of Computer and System Sciences, 1978.

Einfache Inferenzimplementierung vom Hindley-Milner-Typ in C #:

Inferenz vom Hindley-Milner-Typ über (Lisp-ish) S-Ausdrücke in weniger als 650 Zeilen C #

Beachten Sie, dass die Implementierung im Bereich von nur etwa 270 Zeilen C # liegt (für den eigentlichen Algorithmus W und die wenigen Datenstrukturen, die ihn unterstützen).

Verwendungsauszug:

    // ...

    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);

    // ...

... was ergibt:

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.

Siehe auch Brian McKennas JavaScript-Implementierung auf Bitbucket, die auch den Einstieg erleichtert (für mich funktioniert).

'HTH,