В настоящее время я изучаю OCaml, и мне любопытно, КАК OCaml делает свой тип вывода. Я знаю, что это произошло через процесс, называемый унификацией, и я пробовал читать об этом алгоритме в опубликованной статье, но нотация меня отбросила. Может ли кто-нибудь описать шаг за шагом для меня?
Как работает алгоритм определения типа OCaml?
Ответ 1
Собственно, можно утверждать, что унификация - это деталь реализации алгоритма. Система типов - это всего лишь набор правил. Правила позволяют проверить существующий вывод. В правилах не упоминается унификация явно, хотя унификация - это метод, который, естественно, приходит на ум, когда вы думаете о внедрении алгоритма, который автоматически производит вывод типов из выражений.
Мне очень понравилось читать "Функциональное программирование с использованием Caml Light" учебник Michel Mauny, когда у меня был тот же вопрос, что и вы. Учебник показывает свой возраст немного сейчас, но глава, которую вы интересуете (глава 15), по-прежнему так же хороша, как и тогда.
Ответ 2
Каноническая ссылка для изучения вывода типа HM в ML, вероятно, будет Ben Pierce "Типы и языки программирования". Вы можете найти тему, описанную в главе 22 этой книги.
Первый экземпляр алгоритма вывода типа известен как Алгоритм W.
Однако, это может удивить вас, что вы знаете - на самом деле реализация OCaml не просто создает ограничения и решает их! Фактически, он делает гораздо более эффективный алгоритм на основе графа для вывода типа, который (в то время как быстрый) приводит к появлению иногда странных ошибок типа. Вы можете посмотреть ссылки на объяснение ошибок типов в ML.