Co to jest Hindley-Milner?

Spotkałem się z tym terminem Hindley-Milner i nie jestem pewien, czy rozumiem, co to znaczy.

Przeczytałem następujące posty:

• Steve Yegge - Dynamic Languages ​​Strike Back
• Steve Yegge - Problem Pinokia
• Daniel Spiewak - Co to jest Hindley-Milner? (i dlaczego to jest fajne?)

Ale nie ma jednego wpisu dla tego terminu w Wikipedii, gdzie zwykle oferuje mi zwięzłe wyjaśnienie.
^{Uwaga - dodano jeden}

Co to jest?
Jakie języki i narzędzia ją wdrażają lub używają?
Czy mógłbyś udzielić zwięzłej odpowiedzi?

Hindley-Milner to system typów odkryty niezależnie przez Rogera Hindleya (który zajmował się logiką), a później przez Robina Milnera (zajmującego się językami programowania). Zalety Hindley-Milner to

• Obsługuje funkcje polimorficzne ; na przykład funkcja, która może podać długość listy niezależnie od typu elementów lub funkcja przeszukuje drzewo binarne niezależnie od typu kluczy przechowywanych w drzewie.

• Czasami funkcja lub wartość może mieć więcej niż jeden typ , jak w przykładzie funkcji długości: może to być „lista liczb całkowitych do liczby całkowitej”, „lista łańcuchów do liczby całkowitej”, „lista par do liczby całkowitej” itd. na. W tym przypadku zaletą sygnału systemu Hindleya-Milnera jest to, że każdy dobrze wpisany termin ma unikalny typ „najlepszy” , który jest nazywany typem głównym . Głównym typem funkcji długości listy jest „dla dowolnej afunkcji od listy ado liczby całkowitej”. Oto atak zwany „parametr typu”, który jest jawny w rachunku lambda, ale niejawny w większości języków programowania .parametryczny polimorfizm . (Jeśli piszesz definicję funkcji długości w ML, możesz zobaczyć parametr typu w ten sposób:

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

• Jeśli termin ma typ Hindleya-Milnera, wówczas typ główny można wywnioskować bez wymagania jakichkolwiek deklaracji typu lub innych adnotacji ze strony programisty. (To mieszane błogosławieństwo, jak każdy może zaświadczyć, komu kiedykolwiek zajmowano się dużym fragmentem kodu ML bez adnotacji).

Hindley-Milner jest podstawą systemu typów niemal każdego języka funkcjonalnego z typowaniem statycznym. Takie powszechnie używane języki obejmują

• Rodzina ML ( Standard ML i Objective Caml )
• Haskell
• Czysty

Wszystkie te języki rozszerzyły Hindley-Milner; Haskell, Clean i Objective Caml robią to w ambitny i niezwykły sposób. (Rozszerzenia są wymagane, aby poradzić sobie ze zmiennymi zmiennymi, ponieważ podstawowe Hindley-Milner można obalić za pomocą, na przykład, mutowalnej komórki zawierającej listę wartości nieokreślonego typu. Takie problemy są rozwiązywane przez rozszerzenie zwane ograniczeniem wartości ).

Wiele innych mniejszych języków i narzędzi opartych na typowych językach funkcyjnych używa Hindley-Milner.

Hindley-Milner to ograniczenie Systemu F , które dopuszcza więcej typów, ale wymaga adnotacji od programisty .

Możesz znaleźć oryginalne artykuły za pomocą Google Scholar lub CiteSeer - lub lokalnej biblioteki uniwersyteckiej. Pierwszy jest na tyle stary, że być może będziesz musiał znaleźć oprawione kopie czasopisma, nie mogłem go znaleźć w Internecie. Link, który znalazłem dla drugiego, był uszkodzony, ale mogą istnieć inne. Z pewnością będziesz w stanie znaleźć artykuły, które je przytaczają.

Hindley, Roger J, Główny schemat typu obiektu w logice kombinacyjnej , Transactions of the American Mathematical Society, 1969.

Milner, Robin, A Theory of Type Polymorphism , Journal of Computer and System Sciences, 1978.

Prosta implementacja wnioskowania typu Hindley-Milner w C #:

Wnioskowanie o typie Hindleya-Milnera na podstawie (Lisp-ish) S-wyrażeń, w mniej niż 650 wierszach C #

Zauważ, że implementacja mieści się w zakresie tylko 270 wierszy języka C # (w każdym razie dla algorytmu W właściwego i kilku struktur danych do jego obsługi).

Fragment wykorzystania:

    // ...

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

    // ...

... co daje:

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.

Zobacz także implementację JavaScript Briana McKenny w bitbucket, która również pomaga w rozpoczęciu (działała dla mnie).

„HTH,