ΑZ
тут в первом абзаце написано что такое V
Size: a a a
2021 May 26
ΑZ
(лямбды в них не входят (наверное))
ΑZ
понятно что определение рекурсивное
ΑZ
но в итоге оно спускается к аргументам
ΑZ
и применениям
TK
Но непонятно, что оно определяет и является ли корректным в принципе
ΑZ
можешь поверить что является
ΑZ
все современные системы типов построены на этом
TK
Верю, проверить как - не знаю
TK
Был бы пример
AN
exersize for the reader
ΑZ
я дал пример
B
а так There<There<There<Here>>>
ΑZ
x - переменная
10 - терм
правило 1:
x
правило 2:
(y => y)(x)
Правило 3:
(y => something(x,y))
10 - терм
правило 1:
x
правило 2:
(y => y)(x)
Правило 3:
(y => something(x,y))
ΑZ
что тут непонятно?)
AN
оно и есть
TK
Всё понятно, кроме понимания, в чём полезность термов
B
теперь аж свою металибу захотел написать
ΑZ
термы структурно описывают что лямбда делает
ΑZ
как ты без термов это сделаешь?