AG
надо будет запись пересмотреть
Size: a a a
2021 April 12
а
В компиляторах для вывода типов используются специализированные языкт программирования типа пролога, да?
D
Зачем?
к
ну, я недавно услышал шутку "каждый механизм проверки типов содержит корявую и неполную реализацию пролога"
так что в какой-то степени это наверное правда
так что в какой-то степени это наверное правда
а
epic
а
Ну я вот читаю про hindley milner и Algorithm W, там унификация используется и бэктрекинг, похоже на логическое программирование
а
A
Это, видимо, кто-то решил блеснуть эрудицией и переиначил десятое правило Гринспена.
DP
тыдыж в dragon book 2ed в оглавлении datalog есть — как раз в районе раздела про типизацию
DP
не, вру - 12 глава
M
Вывод типа это решения уравнения(ний) с некоторыми условиями через унификацию или любым другим способом который обычно используют при решении constraint solver проблем и соответственно вывод ошибки если решение найти невозможно. Prolog занимается по-сути тем же, только для более широкого класса задач)
а
супер)
ВМ
Я не настоящий сварщик, но как минимум вот прецедент в котором даже слово пролог написано
ВМ
Ещё можно приплести в очередной раз изоморфизм Карри-Говарда
а
О да, про chalk я слышал, интересно
s
Если считать унификацию термов прологом.
а
Знаю такой, а как он к выводу типов относится? 🤔
ВМ
Ну там же прямым текстом говорится что типы можно трактовать как логические утверждения (предикаты)
ВМ
Где-то рядом должен бродить призрак пролога