ما هو هندلي ميلنر؟

Question

واجهت هذا المصطلح هندلي ميلنر, ، ولست متأكدا مما إذا فهم ما يعنيه.

لقد قرأت المشاركات التالية:

• ستيف ييجج - لغات ديناميكية ضربة
• ستيف ييجج - مشكلة pinocchio.
• دانييل Spiewak - ما هو هندلي ميلنر؟ (ولماذا هو بارد؟)

ولكن لا يوجد دخول واحد لهذا المصطلح في ويكيبيديا حيث تقدم لي عادة شرحا موجزا.
^{ملحوظة - واحد لديه تم الآن إضافة}

ما هذا؟
ما اللغات والأدوات التي تنفذها أو استخدامها؟
هل يرجى تقديم إجابة موجزة؟

Answer 1

هندلي ميلنر هو نوع النظام اكتشفت بشكل مستقل عن طريق روجر هندلي (الذي كان ينظر إلى المنطق) وبعد ذلك بواسطة روبن ميلنر (الذي كان ينظر إلى لغات البرمجة). مزايا هندلي ميلنر هي

• انه يدعم متعدد الأشكال المهام؛ على سبيل المثال، وظيفة يمكن أن تعطيك طول القائمة المستقل عن نوع العناصر، أو وظيفة هل يبحث شجرة ثنائية عن نوع المفاتيح المخزنة في الشجرة.

• في بعض الأحيان يمكن أن تحتوي وظيفة أو قيمة أكثر من نوع واحد, ، كما هو الحال في مثال الوظيفة الطول: يمكن أن يكون "قائمة بالأعداد الصحيحة للأعداد الصحيحة"، "قائمة السلاسل إلى عدد صحيح"، "قائمة الأزواج إلى عدد صحيح"، وهلم جرا. في هذه الحالة، ميزة إشارة نظام Hindley-Milner هو ذلك كل مصطلح مكتوب جيدا يحتوي على نوع فريد من نوعه, ، الذي يسمى النوع الرئيسي. وبعد النوع الرئيسي لوظيفة قائمة القائمة هو "لأي a, ، وظيفة من قائمة a إلى عدد صحيح ". هنا a هو ما يسمى "المعلمة النوع"، وهو صريح في حساب التفاضل والتكامل Lambda لكن ضمنية في معظم لغات البرمجة. وبعد يشرح استخدام معلمات النوع لماذا Hindley-Milner هو نظام ينفذ غير رسمي تعدد الأشكال. وبعد (إذا كتبت تعريفا لوظيفة الطول في مل، يمكنك رؤية المعلمة النوع هكذا:

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

• إذا مصطلح يحتوي على نوع هندلي ميلنر، ثم يمكن استنتاج النوع الرئيسي دون مطالبة أي إعلان أو التعليقات التوضيحية الأخرى من قبل المبرمج. (هذه نعمة مختلطة، حيث يمكن لأي شخص أن يشهد من أي وقت مضى تم التعامل مع جزء كبير من رمز ML بدون شرح.)

Hindley-Milner هو أساس نظام النوع من كل لغة وظيفية مكتوبة تقريبا. هذه اللغات في الاستخدام المشترك

• عائلة مل (معيار ML. و كاملا الهدف)
• haskell.
• ينظف

كل هذه اللغات قد امتدت هندلي ميلنر؛ Haskell، نظيفة، وموضوعية Caml تفعل ذلك في طرق طموحة وغير عادية. (ملحقات مطلوبة للتعامل مع المتغيرات القابلة للتغيير، نظرا لأن Milner Basic Hindley-Milner يمكن تخريبها باستخدام، على سبيل المثال، خلية قابلة للتغيير تحمل قائمة قيم نوع غير محدد. يتم التعامل مع هذه المشاكل من خلال امتداد يسمى قيود القيمة.)

العديد من اللغات والأدوات الثانوية الأخرى القائمة على اللغات الوظيفية المكتوبة تستخدم Hindley-Milner.

هندلي ميلنر هو قيود النظام F., ، والتي تسمح المزيد من الأنواع ولكنها يتطلب التعليقات التوضيحية من قبل المبرمج.

Answer 2

قد تتمكن من العثور على الأوراق الأصلية باستخدام عالم Google أو Citesteer - أو مكتبة الجامعات المحلية الخاصة بك. الأول قديم بما يكفي أنه قد تضطر إلى العثور على نسخ ملزمة من المجلة، لم أجدها عبر الإنترنت. الرابط الذي وجدته للآخر قد كسر، ولكن قد يكون هناك آخرون. من المؤكد أنك ستتمكن من العثور على أوراق تشير إلى هذه.

هندلي، روجر ي، مخطط النوع الرئيسي لكائن في المنطق المشترك, ، معاملات الجمعية الأمريكية الرياضية، 1969.

ميلنر، روبن، نظرية من نوع متعدد الأشكال, ، مجلة علوم الكمبيوتر والنظام، 1978.

Answer 3

تطبيق استنتاج هندلي ميلنر بسيط في C #:

استنصاف من نوع Hindley-Millner أكثر من (LISP-ISH) S التعبيرات، في أقل من 650 خطا من C #

لاحظ أن التنفيذ موجود في حدود 270 فقط أو نحو ذلك من خطوط C # (بالنسبة للخوارزمية التي مناسبة وهياكل البيانات القليلة لدعمها، على أي حال).

اقتبام الاستخدام:

    // ...

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

    // ...

... الذي يحصد:

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.

أنظر أيضا تنفيذ جافا سكريبت براين ماكنة على Bitbucket، مما يساعد أيضا في البدء (عملت بالنسبة لي).

'hth،