Dmitry Popov (thedeemon) wrote,
Dmitry Popov
thedeemon

Category:

HM

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

Во-первых, он удивительно хорошо работает. Когда реализуешь такой вывод типов, скормишь ему развесистое дерево программы без единого указания типа, в которой связанные друг с другом по смыслу элементы оказываются очень далеко друг от друга (навроде "функция А передается в функцию Б, где оказывается частью возвращаемого замыкания В, которое передается в Г, вызывается с аргументом типа Д и потому оказывается, что аргумент у А должен быть туплом, у которого первый элемент - функция, принимающая инт"), и твоя реализация ХМ раз-раз и весь пазл сложила и все типы повыводила - это завораживает.

Во-вторых, его удивительно просто сделать. Я сначала не знал, с какой стороны подступиться, правила-то вывода ясны, а вот как именно организовать код не очевидно. Вспомнил про замечательный журнал ПФП, где была статья _darkus_'a с игрушечной реализацией, заглянул туда, и описанный там подход действительно очень прост. У нас есть AST нетипизированной программы, мы хотим узнать тип каждого выражения в нем. Заводим словарик, сопоставляющий разным выражениям какие-то типы. Проходим рекурсивно по AST и все интересующие нас выражения из него складываем в тот словарик. Если тип выражения очевиден сразу (это константа, например), такой и пишем. Если сразу не очевиден - заводим новую типовую переменную (type variable) и пишем ее. А дальше в некоторых местах AST типы подвыражений оказываются связаны друг с другом, например, если значение x передается в функцию f, то его тип должен соответствовать типу аргумента f, или если у нас fst x, то x это тупл, или case x of ..., тогда это сумма типов. В таких местах мы делаем унификацию типов. Эта процедура берет текущее состояние словарика (контекста) и два типа, и сопоставляет их друг с другом: если это константы, они должны совпадать, если это сложные типы вроде функций, произведений или сумм, они должны иметь одну форму и должны унифицироваться соответсвующие части, наконец если один из сопоставляемых типов - типовая переменная, то это значит мы только что узнали чему она равна, и мы везде в словарике можем ее заменить на ее новое значение (второй переданный в процедуру унификации тип). В результате после успешной унификации двух типов у нас количество используемых типовых переменных может уменьшиться, на их месте в словарике окажутся более уточненные типы. И этого процесса достаточно, чтобы все повыводить в корректной программе.

А третья удивительная вещь в таком выводе типов - его удивительно сложно реализовать правильно. При всей его простоте, я за одним багом несколько дней гонялся. И у _darkus_'a в статье он тоже присутствует, насколько я понимаю. Фишка вот в чем. Если мы унифицируем два составных типа вроде функций, произведений или сумм, например X1 -> Y1 и X2 -> Y2, то нам надо унифицировать X1 с X2, и Y1 с Y2. Мы вызываем функцию унификации сначала для одной пары, потом для второй, всего и делов, так?
unifyTypes (Arrow t1 t2, Arrow t1' t2') env
  = do env' <- unifyTypes (t1, t1') env
       unifyTypes (t2, t2') env'
(цитата из статьи Душкина)
А вот фиг. Пусть у нас есть типовые переменные t1 и t2, и переданы значения X1=t1, X2=Int, Y1=t1, Y2=t2. После унификации X1 с X2 типовая переменная t1 обретет свое значение - Int - и будет убрана из словарика (везде будет заменена на Int), а потом мы делаем унификацию Y1 с Y2, где Y1=t1, она заменяется на t2, результат запоминается в словарике-контексте, и вот у нас в нем оказалась неразрешенная типовая переменная, хотя очевидно, что t2 это тоже Int. При правильном подходе производить подстановки нужно не только в словарике-контексте, но и в переданных для унификации типах.

Такой вот трижды удивительный алгоритм.

PS. Успехов всем на ICFPC, который начнется... уже через -13 минут!
Tags: fp
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your IP address will be recorded 

  • 9 comments