Apa itu Hindley-Milner?

Saya menemukan istilah ini Hindley-Milner , dan saya tidak yakin apakah mengerti artinya.

Saya telah membaca posting berikut:

• Steve Yegge - Dynamic Languages ​​Strike Back
• Steve Yegge - Masalah Pinokio
• Daniel Spiewak - Apakah Hindley-Milner itu? (dan mengapa itu keren?)

Tetapi tidak ada entri tunggal untuk istilah ini di wikipedia yang biasanya menawarkan saya penjelasan singkat.
^{Catatan - sekarang telah ditambahkan}

Apa itu?
Bahasa dan alat apa yang menerapkan atau menggunakannya?
Bisakah Anda memberikan jawaban yang ringkas?

Hindley-Milner adalah sistem tipe yang ditemukan secara independen oleh Roger Hindley (yang melihat logika) dan kemudian oleh Robin Milner (yang mempelajari bahasa pemrograman). Kelebihan Hindley-Milner adalah

• Ini mendukung fungsi polimorfik ; misalnya, fungsi yang dapat memberi Anda panjang daftar terlepas dari jenis elemen, atau fungsi melakukan pencarian pohon biner terlepas dari jenis kunci yang disimpan di pohon.

• Terkadang fungsi atau nilai dapat memiliki lebih dari satu jenis , seperti pada contoh fungsi panjang: dapat berupa "daftar bilangan bulat menjadi bilangan bulat", "daftar string ke bilangan bulat", "daftar pasangan ke bilangan bulat", dan sebagainya di. Dalam hal ini, keuntungan sinyal dari sistem Hindley-Milner adalah bahwa setiap istilah yang diketik dengan baik memiliki tipe "terbaik" yang unik , yang disebut tipe utama . Jenis utama dari fungsi panjang-daftar adalah "untuk setiap a, fungsi dari daftar ake bilangan bulat". Berikut aini yang disebut "parameter tipe", yang eksplisit dalam kalkulus lambda tetapi tersirat di sebagian besar bahasa pemrograman . polimorfisme parametrik . (Jika Anda menulis definisi fungsi panjang dalam ML,

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

• Jika sebuah istilah memiliki tipe Hindley-Milner, maka tipe utama dapat disimpulkan tanpa memerlukan deklarasi tipe atau penjelasan lain oleh programmer. (Ini adalah berkah campuran, karena siapa pun dapat membuktikan siapa yang pernah ditangani sebagian besar kode ML tanpa anotasi.)

Hindley-Milner adalah dasar untuk sistem tipe dari hampir setiap bahasa fungsional yang diketik secara statis. Bahasa yang umum digunakan termasuk

• Keluarga ML ( ML Standar dan Objective Caml )
• Haskell
• Bersih

Semua bahasa ini telah memperluas Hindley-Milner; Haskell, Clean, dan Objective Caml melakukannya dengan cara yang ambisius dan tidak biasa. (Ekstensi diperlukan untuk menangani variabel yang dapat berubah, karena Hindley-Milner dasar dapat ditumbangkan menggunakan, misalnya, sel yang dapat diubah yang menyimpan daftar nilai jenis yang tidak ditentukan. Masalah tersebut ditangani dengan ekstensi yang disebut pembatasan nilai .)

Banyak bahasa dan alat minor lainnya yang didasarkan pada bahasa fungsional yang diketik menggunakan Hindley-Milner.

Hindley-Milner adalah batasan dari Sistem F , yang memungkinkan lebih banyak tipe tetapi membutuhkan penjelasan oleh programmer .

Anda mungkin dapat menemukan makalah asli menggunakan Google Scholar atau CiteSeer - atau perpustakaan universitas setempat Anda. Yang pertama cukup tua sehingga Anda mungkin harus menemukan salinan jurnal yang terikat, saya tidak dapat menemukannya secara online. Tautan yang saya temukan untuk yang lain rusak, tetapi mungkin ada yang lain. Anda pasti bisa menemukan makalah yang mengutip ini.

Hindley, Roger J, Skema tipe utama dari suatu objek dalam logika kombinatori , Transactions of the American Mathematical Society, 1969.

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

Implementasi inferensi tipe Hindley-Milner sederhana di C #:

Jenis inferensi Hindley-Milner atas ekspresi S (Lisp-ish), di bawah 650 baris C #

Perhatikan bahwa implementasinya hanya berkisar 270 baris C # (untuk algoritme W yang sesuai dan beberapa struktur data yang mendukungnya).

Kutipan penggunaan:

    // ...

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

    // ...

... yang menghasilkan:

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.

Lihat juga implementasi JavaScript Brian McKenna di bitbucket, yang juga membantu untuk memulai (berhasil untuk saya).

'HTH,