Co to jest Hindley-Milner?


124

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

Przeczytałem następujące posty:

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?

Odpowiedzi:


167

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ą

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 .


2
@NormanRamsey Wiem, że to jest okropne stare, ale dzięki za wyjaśnienie tego, co mnie denerwuje bez końca: za każdym razem, gdy mówię o systemie typu Hindley-Milner, ktoś dzwoni, mówiąc o wnioskowaniu typu, do tego stopnia, że ​​zacząłem kwestionować, czy HM jest typem system lub po prostu algorytm wnioskowania ... Dziękuję, jak sądzę, na wikipedii za dezinformowanie ludzi o tym do tego stopnia, że ​​nawet mnie zmyliły ..
Jimmy Hoffa

1
Dlaczego jest parametrycznie polimorficzny, w przeciwieństwie do po prostu polimorficznego? Przykład z Any, który podałeś, widzę jako przykład jeśli polimorfizm - gdzie podtypy mogą być używane zamiast nadtypu, który jest określony w definicji, a nie polimorfizm parametryczny ala C ++, gdzie rzeczywisty typ jest określony przez programistę w celu utworzenia nowa funkcja.
corazza

1
@jcora: Kilka lat później, ale z korzyścią dla przyszłych czytelników: nazywa się to polimorfizmem parametrycznym ze względu na właściwość parametryczności , co oznacza, że ​​dla każdego typu, który podłączysz, wszystkie wystąpienia takiej funkcji length :: forall a. [a] -> Intmuszą zachowywać się tak samo, niezależnie od a- to jest nieprzezroczysty; nic o tym nie wiesz. Nie ma instanceof(Java generics) ani „duck typing” (szablony C ++), chyba że dodasz dodatkowe ograniczenia typu (typeklasy Haskell). Dzięki parametryczności można uzyskać niezłe dowody na to, co dokładnie funkcja może / nie może zrobić.
Jon Purdy,

8

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.


2
Ten ostatni można znaleźć tutaj: citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.67.5276
Magnus


6

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,

Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.