html текст
All interests
  • All interests
  • Design
  • Food
  • Gadgets
  • Humor
  • News
  • Photo
  • Travel
  • Video
Click to see the next recommended page
Like it
Don't like
Add to Favorites

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

Как-то мы сидели в баре с Джошем Лонгом и ещё несколькими друзьями с работы, когда он обнаружил, что я на «эй, ты!» с математикой. А он как раз недавно наткнулся на вот этот вопрос на StackOverflow и сейчас спросил меня, что это означает:



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

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

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


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

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

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

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

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

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

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


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


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

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


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

материал с habrahabr.ru

3

      Add

      You can create thematic collections and keep, for instance, all recipes in one place so you will never lose them.

      No images found
      Previous Next 0 / 0
      500
      • Advertisement
      • Animals
      • Architecture
      • Art
      • Auto
      • Aviation
      • Books
      • Cartoons
      • Celebrities
      • Children
      • Culture
      • Design
      • Economics
      • Education
      • Entertainment
      • Fashion
      • Fitness
      • Food
      • Gadgets
      • Games
      • Health
      • History
      • Hobby
      • Humor
      • Interior
      • Moto
      • Movies
      • Music
      • Nature
      • News
      • Photo
      • Pictures
      • Politics
      • Psychology
      • Science
      • Society
      • Sport
      • Technology
      • Travel
      • Video
      • Weapons
      • Web
      • Work
        Submit
        Valid formats are JPG, PNG, GIF.
        Not more than 5 Мb, please.
        30
        surfingbird.ru/site/
        RSS format guidelines
        500
        • Advertisement
        • Animals
        • Architecture
        • Art
        • Auto
        • Aviation
        • Books
        • Cartoons
        • Celebrities
        • Children
        • Culture
        • Design
        • Economics
        • Education
        • Entertainment
        • Fashion
        • Fitness
        • Food
        • Gadgets
        • Games
        • Health
        • History
        • Hobby
        • Humor
        • Interior
        • Moto
        • Movies
        • Music
        • Nature
        • News
        • Photo
        • Pictures
        • Politics
        • Psychology
        • Science
        • Society
        • Sport
        • Technology
        • Travel
        • Video
        • Weapons
        • Web
        • Work

          Submit

          Thank you! Wait for moderation.

          Тебе это не нравится?

          You can block the domain, tag, user or channel, and we'll stop recommend it to you. You can always unblock them in your settings.

          • habrahabr.ru
          • домен habrahabr.ru

          Get a link

          Спасибо, твоя жалоба принята.

          Log on to Surfingbird

          Recover
          Sign up

          or

          Welcome to Surfingbird.com!

          You'll find thousands of interesting pages, photos, and videos inside.
          Join!

          • Personal
            recommendations

          • Stash
            interesting and useful stuff

          • Anywhere,
            anytime

          Do we already know you? Login or restore the password.

          Close

          Add to collection

             

            Facebook

            Ваш профиль на рассмотрении, обновите страницу через несколько секунд

            Facebook

            К сожалению, вы не попадаете под условия акции