Что такое Хиндли-Милнер? - PullRequest
       100

Что такое Хиндли-Милнер?

117 голосов
/ 30 декабря 2008

Я встречал этот термин Хиндли-Милнер , и я не уверен, что понял, что это значит.

Я прочитал следующие сообщения:

Но в википедии нет единой записи для этого термина, где обычно дается краткое объяснение.
Примечание - теперь добавлено

Что это?
Какие языки и инструменты реализуют или используют его?
Не могли бы вы предложить краткий ответ?

Ответы [ 3 ]

156 голосов
/ 30 декабря 2008

Хиндли-Милнер - это система типа , открытая независимо Роджером Хиндли (который смотрел на логику), а затем Робином Милнером (который смотрел на языки программирования). Преимущества Хиндли-Милнера:

  • Поддерживает полиморфные функции; например, функция, которая может дать вам длину списка независимо от типа элементов, или функция выполняет поиск в двоичном дереве независимо от типа ключей, хранящихся в дереве.

  • Иногда функция или значение могут иметь более одного типа , как в примере с функцией длины: это может быть «список целых чисел в целое число», «список строк в целое число» "," список пар целых чисел "и так далее. В этом случае сигнальным преимуществом системы Хиндли-Милнера является то, что каждый хорошо типизированный термин имеет уникальный «лучший» тип , который называется основной тип . Основным типом функции длины списка является «для любой a, функция из списка от a до целого числа». Здесь a - это так называемый «параметр типа», который явный в лямбда-исчислении , но неявный в большинстве языков программирования . Использование параметров типа объясняет, почему Хиндли-Милнер является системой, которая реализует параметрический полиморфизм . (Если вы напишите определение функции длины в ML, вы можете увидеть параметр типа следующим образом:

     fun 'a length []      = 0
       | 'a length (x::xs) = 1 + length xs
    
  • Если термин имеет тип Хиндли-Милнера, то основной тип может быть выведен без каких-либо объявлений типа или других аннотаций программистом. (Это смешанное благословение, так как любой может засвидетельствовать, кто когда-либо обрабатывал большой кусок кода ML без аннотаций.)

Хиндли-Мильнер является основой системы типов почти каждого статически типизированного функционального языка. К таким языкам общего пользования относятся

Все эти языки расширились Хиндли-Милнер; Haskell, Clean и Objective Caml делают это амбициозными и необычными способами. (Расширения требуются для работы с изменяемыми переменными, поскольку базовый Хиндли-Милнер может быть подорван с использованием, например, изменяемой ячейки, содержащей список значений неопределенного типа. Такие проблемы решаются расширением, называемым значение ограничения .)

Многие другие второстепенные языки и инструменты, основанные на типизированных функциональных языках, используют Хиндли-Милнера.

Хиндли-Милнер - это ограничение Система F , которое допускает большее количество типов, но для которого требуется аннотирование программистом .

8 голосов
/ 30 декабря 2008

Вы можете найти оригинальные документы, используя Google Scholar или CiteSeer - или вашу местную университетскую библиотеку. Первый достаточно старый, чтобы вам приходилось искать переплетенные копии журнала, я не смог найти его в Интернете. Ссылка, которую я нашел для другой, была сломана, но могут быть и другие. Вы наверняка сможете найти документы, которые ссылаются на них.

Хиндли, Роджер Дж., Принципиальная схема типа объекта в комбинаторной логике , Труды Американского математического общества, 1969 г.

Милнер, Робин, Теория полиморфизма типов , Журнал компьютерных и системных наук, 1978.

5 голосов
/ 04 июля 2012

Простая реализация логического вывода типа Хиндли-Милнера в C #:

Вывод типа Хиндли-Милнера по S-выражениям (Lisp-ish), менее чем в 650 строках C #

Обратите внимание, что реализация находится в диапазоне только 270 или около того строк C # (во всяком случае, для собственно алгоритма W и нескольких структур данных для его поддержки).

Выдержка из использования:

    // ...

    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.

См. Также Реализация JavaScript Брайана МакКенны в битбакете, которая также помогает начать работу (работал для меня).

НТН,

...