Итак, вы всё ещё не понимаете Хиндли-Милнера? Часть 1

http://akgupta.ca/blog/2013/05/14/so-you-still-dont-understand-hindley-milner/
  • Перевод
Как-то мы сидели в баре с Джошем Лонгом и ещё несколькими друзьями с работы, когда он обнаружил, что я на «эй, ты!» с математикой. А он как раз недавно наткнулся на вот этот вопрос на StackOverflow и сейчас спросил меня, что это означает:



Однако, перед выяснением смысла данной китайской грамоты, думаю, стоит в принципе получить представление о том, для чего вообще это нужно. Пост в блоге Даниэля Спивака (перевод) даёт по-настоящему хорошее объяснение конечной цели алгоритма Хиндли-Милнера (в дополнение к углубленному примеру его применения):
Функционально говоря, Хиндли-Милнер (или Дамас-Милнер) — это алгоритм для вывода типов, основанный на рассмотрении того, как они используются. Он буквально формализует интуитивное знание о том, что тип может быть выведен через функционал, который он поддерживает.

Итак, мы хотим формализовать алгоритм вывода типа для любого заданного выражения. В этом посте я собираюсь остановиться на том, что означает «формализовать что-то», а затем описать «кирпичики» формализации Хиндли-Милнера. Во второй части я дам более конкретное описание этих блоков. Наконец, в третьей части я переведу вопрос со StackOverflow.

Что означает «формализовать»?


Итак, мы собираемся говорить о выражениях. Произвольных выражениях. На произвольном языке. А ещё мы хотим поговорить о выводе типов для этих выражений. И мы хотим выяснить правила, по которым мы смогли бы выводить типы. А затем мы хотим создать алгоритм, который использовал бы эти правила для вывода типов. Таким образом, нам нужен некий мета-язык. Такой, чтобы с его помощью можно было говорить о выражении на любом произвольном языке программирования. Этот мета-язык должен:
  • Быть абстрактным и общим для того, чтобы позволить нам рассуждать об утверждениях вывода типа, исходя исключительно из их формы (отсюда формализация), не заботясь о содержании
  • Давать точное, однозначное, но интуитивно понятное определение того, чем выражение является
  • Давать это определение в терминах малого числа бесспорных примитивных понятий
  • Аналогичным образом давать определение для типов, идею того, что выражение имеет тип, и идею, что мы можем вывести положение о том, что данное выражение имеет данный тип
  • Поддаваться простому, краткому символическому представлению. Т.е. вместо того, чтобы говорить «выражение, сформированное путём применения первого выражения к второму выражению, имеет тип функции от строки к какому-то типу, который нам нет необходимости специализировать в данном контексте», мы можем просто сказать "e1(e2):Stringt"
  • Легко транслироваться во что-то, что компьютер может понять и реализовать, чтобы могли полностью автоматизировать вывод типов

Чтобы придать вышесказанному больше конкретики, давайте рассмотрим очень короткий пример формализации. Что если вместо того, чтобы формализовать язык для разговора о выводе типов выражений в произвольном языке программирования, мы захотим формализовать язык для разговора об истинности высказывания на произвольном естественном языке? Без формализации мы могли бы сказать что-то вроде:
Предположим, я знаю, что если идёт дождь, то Боб всегда берёт зонт.
И предположим, что я знаю, что сейчас идёт дождь.
Таким образом, я могу заключить, что Боб взял зонт.

И любой аргумент, имеющий эту же форму, является допустимым для подобного вывода.

Исчисление высказываний формализует все эти вещи в виде правила, известного как Modus Ponens («правило вывода»):

где А и В — переменные, представляющие утверждения (a.k.a. предложения или положения) в произвольном естественном языке.

А теперь давайте перечислим строительные блоки формализации Хиндли-Милнера:

Строительные блоки формализации


Нам потребуются:
  1. Формальный способ, чтобы говорить о выражениях. Эта формализация должна соответствовать критериям, перечисленным выше; для этой цели мы используем лямбда-исчисление. Я всё объясню буквально через минуту, но тут нет ничего сверхъестественного
  2. Формальный способ, чтобы говорить о типах, и формальный способ, чтобы говорить о типах и выражениях вместе. В конце-концов, цель алгоритма Хиндли-Милнера — быть способным вывести заключение вида «выражение e имеет тип t»
  3. Формальный набор правил для получения утверждений о типе выражения через другие утверждения. Эти правила наподобие: «если я уже могу продемонстрировать, что некое выражение имеет один тип, а другое выражение — второй тип, то третье выражение будет иметь третий тип». Такой набор правил — в точности то, что вы видите в вопросе со StackOverflow. Я переведу его во всех подробностях
  4. Алгоритм должен разумно использовать правила вывода, чтобы из отправной точки вывести требуемое утверждение: «Интересующее меня выражение e имеет тип t». За это отвечает часть «алгоритм» в словосочетании «алгоритм Хиндли-Милнера», и в этих постах я не планирую обсуждать этот вопрос.


Чтож, поехали!

  • Часть 2, в которой мы чётко определимся по пунктам 1 и 2
  • Часть 3, в которой мы переведём правила вывода типов из пункта 3


Примечание переводчика: я буду очень признательна за любые замечания в личку по поводу перевода.
Поделиться публикацией

Похожие публикации

Комментарии 14
    0
    А где и для чего на практике это можно использовать?
      0
      «А где и для чего на практике это можно использовать?»
      var x = await MySheduler.FirstTask.Start();

      по сути идет формализация правил «вывода типов». Немножко матлогики и мы получаем все, что нужно.
      Г ⊢ X: T означает, что «из гипотезы Г выводится то, что X принадлежит типу T» Значек ⊢ — это перевернутая «Т», от слова «Теорема». То есть существует теорема, доказывающее подобный вывод.
        +1
        Автовывод из C# (var) и C++ (auto) не демонстрирует всего масштаба «трагедии». Пример на Haskell:
        inums = [0..5]
        fnums = [0..5]
        
        main = do
             print inums
             let fprint = print :: [Double] -> IO ()
             fprint fnums
        

        Вывод:
        [0,1,2,3,4,5]
        [0.0,1.0,2.0,3.0,4.0,5.0]
        

        Несмотря на то, что именам inum и fnum были присвоены одинаковые выражения, компилятор вывел им разные типы, используя информацию в контексте их использования. Ни C#, ни C++, ни Scala такого не могут. Одна из впечатляющих демонстраций мощи системы типов в Haskell — модуль регулярных выражений, в котором один оператор =~ может возвращать разные типы значений в зависимости от контекста использования, и это всё преспокойно вписывается в систему типов (Regular expressions in Haskell). В RWH есть ещё впечатляющий пример с построением AST из арифметики: Extended example: Numeric Types.
          –2
          var inums = Enumerable.Range(0, 6).ToList();
          var fnums = Enumerable.Range(0, 6).ToList();
          inums.ForEach(Console.WriteLine);
          Action fprint = i => Console.WriteLine((double) i);
          fnums.ForEach(fprint);

          честно говоря не увидел, что намного мощнее. Лаконичнее — да, но это не во всем. Когда изучал функциональщину то тоже показалось, что вывод всего и вся, иммутабельность, сопоставление с образцом — все очень красиво и кратко. А когда решил реальную задачу попробовать смастерить — любимый шарп дал 100 очков форы. Конечно, можно сказать, что я плохо знаю функциональные языки, но результат ООП + лямбда-выражений зачастую оказывается не хуже, а иногда и лучше.

          P.S. (почему-то теги так и не хотят работать… Видимо, репутация и на это влияет :( )
            +1
            Между моим примером и вашим на самом деле есть принципиальная разница: в моём примере у выражений разный статический тип, а в вашем он одинаков, поэтому вам пришлось написать копию функции с рантайм-кастом. Это совсем не то.
            Я не питаю иллюзий по поводу функциональщины, этап эйфории прошёл пару лет назад. Я видел реальный функциональный код, и мне часто сложно назвать его красивым и кратким. Мой текущий рабочий язык C++, а ради удовольствия я иногда пишу на Go, периодически балуясь функциональными языками. Но функциональные идеи очень сильно повлияли на меня и на мой стиль программирования. Это незаменимая школа дизайна.
              0
              Насчет школы и дизайна — абсолютно согласен. По крайней мере делегаты и локальные лямбды теперь используются намного чаще, а код — получается намного чище.

              А вот насчет принципиальной разницы не особо понял. Может поясните более конкретно? Насколько я понял, у вас просто получается неявное преобразование Action к Action, этакая ковариация типа делегата, в шарпе это запрещено, то есть
              пусть T: U, но тогда ⌐∀T (Generic(T): Generic(U)), то есть такую ковариацию можно произвести не для всех типов, а только для наследников, причем делегаты должны быть явно указанны как ковариационные. В шарпе, очевидно, int не является наследником double и наоборот тоже.

              Либо я опять вас не понял)
                0
                неявное преобразование Action к Action

                Нет, let в коде нужен только для того, чтобы создать контекст, в котором требуется [Double]. Вот другой пример:

                inum = [0..5]
                fnum = [0..5]
                
                sins = map sin
                
                printNums = do
                          print inum
                          print $ sins fnum
                


                Загружаем в интерпретаторе:
                Prelude> :load "HM.hs"
                [1 of 1] Compiling Main             ( HM.hs, interpreted )
                Ok, modules loaded: Main.
                *Main> :t inum
                inum :: [Integer]
                *Main> :t fnum
                fnum :: [Double]
                

                Видите, компилятор вывел для inum и fnum разные статические типы. Т.е. не вставил каст из [Integer] в [Double], а именно изначално присвоил именам правильный статический тип. Он считает, что inum — это список целых, а fnum — список чисел с плавающей точкой, не смотря на то, что им присвоено одно и тоже выражение. У вас же и inum и fnum имеют один и тот же статический тип, компилятор c# считает их оба чем-то вроде IEnumerable<int>.
                  –2
                  Посмотрите ниже. Для языков типа шарпа недостаточно знать, что это «целое» или «с плавающей запятой» Это может быть short, может быть byte, может быть знаковый или беззнаковый… Много чего может быть. И в общем случае задача вывода нетривиальная. Тут это наверняка как-то по-хитрому решается (сложнее, чем в примере выше, потому что там все-таки не охватывается все многообразие имо), но тут у нас остается какая-то степень контроля над программой (множество возможных значений числа, занимаемый объем памяти, и т.д.). В хаскелле афайк вообще длинная арифметика реализована неявно, а вот в том же шарпе всему этому приходится уделять внимание, я бы не сказал, что это сделано по недосмотру или небрежности.
                    +2
                    Вы так говорите, будто в Haskell нет аналогов short и byte. Для длинной арифметики в Haskell есть тип Integer (используемый по умолчанию), есть и обычный Int. Типы Integer и Double выбраны исключительно в целях демонстрации.

                    По шагам логика компиляторов:
                    C#: о, переменной неуказанного типа присвоили значение типа X. Значит, её типом будет X.
                    Haskell: Ага, эту переменную инициализируют списком числовых констант. А ещё её используют в контексте, где требуется список чисел с плавающей точкой. Хм, чтобы типы в модуле сходились, тип переменной должен быть [Double], т.к. [Double] можно проинициализировать числовыми константами и передать в соответствующую функцию.

                    В реальности условия, рассматриваемые для вычисления оптимального типа, могут быть значительно более сложными и их может быть больше. Например, Haskell без труда вычисляет тип рекурсивных функций.
                      0
                      Круто. Даже не представляю, каким адским матаном это все реализовывалось. Вернее, матлогикой. Вернее даже представляю. Но просыпаться в холодном поту не хочу. Так что поверю вам на слово.
                  0
                  делегаты и локальные лямбды

                  Я имел в виду несколько большее, чем сахар лямбд.

                  Ленивые вычисления, монады (например, в контексте асинхронных и ленивых вычислений), функции высшего порядка и комбинаторы (один из моих любимых приёмов; IEnumerator можно считать примером программирования с помощью комбинаторов), классы типов (typeclasses), разделение «чистых» функций и функций с побочными эффектами, недетерминированные вычисления… Несчётное множество приёмов, которые можно применить независимо от языка, на котором пишешь.
                    –2
                    Почти все это реализовано в шарпе, только местами немного кривокосо (напиример, «чистые» функции отличаются от обычных только добавлением аттрибута [Pure]).

                    Так что надеемся на развитие.

                    «Я имел в виду несколько большее, чем сахар лямбд.»
                    Ну так и я не про то, чтобы писать на 2 строчки меньше кода, а про то, что у меня иногда встречаются функции, которые принимают параметрами функции, которые работают с функциями. Не скажу, что это часто нужно, обычно это все же излишне, но например как в задаче многомерной нелинейной оптимизации, где целевая функция у нас в свою очередь имеет аргументом другие функции, это является насущной необходимостью
                  0
                  В шарпе многие подобные вещи запрещены, по причине того, что иногда неясно, какой тип должен быть у делегата
                  stackoverflow.com/questions/4965576/why-cant-an-anonymous-method-be-assigned-to-var
            +2
            Хиндли-Милнер это один из самых популярных механизмов вывода типов в языках, поддерживающих функциональное программирование. Понять его на интуитивном уровне гораздо проще, чем кажется: находим использования символа в исходном коде и решаем систему уравнений в типах, используя самый общий тип в качестве решения. Он используется в компиляторах ML, OCaml и Haskell. Он позволяет практически не писать тэги типов, и, тем не менее, гарантировать типобезопасность. Scala, например, ради ООП пошла своим путём в выводе типов, который, на мой взгляд, гораздо менее прозрачен, чем в Haskell.

          Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.

          Самое читаемое