p
Мне нравится идея сначала выучить теорию типов
Ну для такого транспилятора не нужна потому что тут не надо создавать язык, только компилятор готового
Size: a a a
2020 August 28
p
на идрисе пишет хотя бы 10 человек?
Что значит пишет?
SP
на идрисе пишет хотя бы 10 человек?
дело не в том скока на чем пишет. дело в том что ты получаешь имея такой инструмент
H
дело не в том скока на чем пишет. дело в том что ты получаешь имея такой инструмент
Если на нём пишет мало, ты получаешь отсутствие экосистемы и баги в компиляторе
SP
экстраверсивные войсобляди угнетают
H
А свободные переменные в нотации Де Брейна как указываются?
KR
А свободные переменные в нотации Де Брейна как указываются?
В статье написано же.
Или это "сам спросил, сам ответил"?
Или это "сам спросил, сам ответил"?
KR
A variable n is bound if it is in the scope of at least n binders (λ); otherwise it is free.
H
A variable n is bound if it is in the scope of at least n binders (λ); otherwise it is free.
Я не понял это
H
то есть 99999999999999999999999 — значит свободная переменная?
KR
Если у тебя нет столько лямбд перед ней, то да
H
Странно, но я понял
KR
Странно, но я понял
Ну, типа оперируешь глубинами вместо x/y
H
И подстановка сложная какая-то, но зато альфа-эквивалентность есть синтаксическое равенство
KR
Да, прикол разных нотаций в разном угле зрения на одно и то же)
H
Ладно, просто буду использовать именованные связки
KR
Кек...