Что такое Хиндли-Милнер?
-
29-08-2019 - |
Вопрос
Я столкнулся с этим термином Хиндли-Милнер, и я не уверен, что понимаю, что это значит.
Я прочитал следующие посты:
- Стив Йегге - Динамические языки Наносят Ответный удар
- Стив Йегге - Проблема с Пиноккио
- Дэниел Спивак - Что такое Хиндли-Милнер?(и почему это круто?)
Но в википедии нет ни одной записи для этого термина, где обычно давалось бы мне краткое объяснение.
Примечание - у одного есть теперь добавлено
Что это такое?
Какие языки и инструменты реализуют или используют это?
Не могли бы вы, пожалуйста, дать краткий ответ?
Решение
Хиндли-Милнер - это система типов обнаружен независимо Роджером Хиндли (который изучал логику) и позже Робином Милнером (который изучал языки программирования).Преимущества Hindley-Milner заключаются в следующем
Он поддерживает полиморфный функции;например, функция, которая может указать вам длину списка независимо от типа элементов, или функция, выполняющая поиск в двоичном дереве независимо от типа ключей, хранящихся в дереве.
Иногда функция или значение могут иметь более одного типа, как в примере с функцией длины:это может быть "список целых чисел в integer", "список строк в integer", "список пар в integer" и так далее.В этом случае существенным преимуществом системы Хиндли-Милнера является то, что каждый хорошо типизированный термин имеет уникальный "лучший" тип, который называется основной тип.Основным типом функции длины списка является "для любого
a
, функция из спискаa
к целому числу".Здесьa
является так называемым "параметром типа", который является явный в лямбда - исчислении но неявный в большинстве языков программирования.Использование параметров типа объясняет, почему Hindley-Milner - это система, которая реализует параметрический полиморфизм.(Если вы напишете определение функции длины в ML, вы можете увидеть параметр type таким образом:fun 'a length [] = 0 | 'a length (x::xs) = 1 + length xs
Если термин имеет тип Хиндли-Милнера, тогда основной тип может быть выведен без каких-либо объявлений типа или другие аннотации программиста.(Это смешанное благословение, как может подтвердить любой, кто когда-либо работал с большим куском ML-кода без аннотаций.)
Хиндли-Милнер является основой для системы типов почти каждого статически типизированного функционального языка.К таким широко используемым языкам относятся
- Семейство ML (Стандартный МЛ и Объективный Caml)
- Хаскелл
- Чистый
Все эти языки расширили Хиндли-Милнер;Haskell, Clean и Objective Caml делают это амбициозными и необычными способами.(Расширения требуются для работы с изменяемыми переменными, поскольку базовый вариант Хиндли-Милнера можно изменить, используя, например, изменяемую ячейку, содержащую список значений неопределенного типа.Такие проблемы решаются с помощью расширения, называемого ограничение стоимости.)
Многие другие второстепенные языки и инструменты, основанные на типизированных функциональных языках, используют Hindley-Milner.
Хиндли-Милнер - это ограничение Система F, который допускает больше типов , но который требуются аннотации от программиста.
Другие советы
Возможно, вы сможете найти оригиналы статей с помощью Google Scholar или CiteSeer - или в местной университетской библиотеке.Первый достаточно старый, чтобы вам, возможно, пришлось найти переплетенные экземпляры журнала, я не смог найти его в Интернете.Ссылка, которую я нашел для другой, была разорвана, но могли быть и другие.Вы наверняка сможете найти статьи, в которых это цитируется.
Хиндли, Роджер Дж., Схема основного типа объекта в комбинаторной логике, Труды Американского математического общества, 1969.
Милнер, Робин, Теория полиморфизма типов, Журнал компьютерных и системных наук, 1978.
Простая реализация вывода типа Хиндли-Милнера на C# :
Вывод типа Хиндли-Милнера по S-выражениям (на языке Lisp), менее чем в 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 на bitbucket, который также помогает начать работу (у меня сработало).
'ХТХ,