Comments 5
Почему мне все время хочется назвать «Г» — гамма-функцией Эйлера?
Честно говоря думал, что здесь скрыт куда более сакральный смысл связанный с теорвером.
Честно говоря думал, что здесь скрыт куда более сакральный смысл связанный с теорвером.
Г — это гипотеза. То есть Г ⊢ X: T означает, что «из гипотезы Г выводится то, что X принадлежит типу T»
Это можно переписать в виду: ⊢ Г => X: T, то есть «Формула, что из гипотезы Г следует то, что X принадлежит типу T, является общезначимой». Общезначимая формула, по сути, это аксиома. Очевидно, что эти две записи эквивалентны.
Это можно переписать в виду: ⊢ Г => X: T, то есть «Формула, что из гипотезы Г следует то, что X принадлежит типу T, является общезначимой». Общезначимая формула, по сути, это аксиома. Очевидно, что эти две записи эквивалентны.
Да, с сакральным смыслом выражения обломали :). Но все равно спасибо за статью, новые знания не повредят.
Спасибо
Спасибо за ваши переводы. Позволю себе оставить здесь ссылку на статью Душкина, которая помогла мне когда-то лучше понять Хиндли-Милнера. Там, кстати, приведена реализация алгоритма на Haskell.
Sign up to leave a comment.
Итак, вы всё ещё не понимаете Хиндли-Милнера? Часть 3