A
Ясно, спасибо.
Вот! У меня есть вопрос как раз для этой группы специалистов по ФП!
Почему автор функционального языка Dhall реализовал у себя в ЯП только операции сложения и умножения? Даже вычитание запретил.
Size: a a a
2020 September 21
AV
ВЫЧИТАНИЕ ЭТО СЛОЖНО
AV
(это не шутка)
AI
любая обратная операция сложно
PS
ВЫЧИТАНИЕ ЭТО СЛОЖНО
Сложно в смысле разрешимости? То есть автор ориентировался на арифметику Пресбургера? :)
AV
У него кстати Natural только? (тогда надо тащить доказательства) или Integer тоже есть?
PS
Integer тоже есть.
PS
любая обратная операция сложно
Не для АЛУ процессора :)
AV
Кстати, negate для Integer есть
AI
использовать встроенное вычитание АЛУ работающее с двоичным представлением чисел - читерство при создании своего ФЯ )
AV
let example7 = assert : subtract +3 -5 ≡ -8сразу понятно!
PS
Кстати, negate для Integer есть
Да. Я в целом логику автора хочу понять. Он нигде не пишет, что собирается доказывать код на Dhall. Все, что рекламируется — отсутствие проблемы останова.
PS
let example7 = assert : subtract +3 -5 ≡ -8сразу понятно!
Да, операнды перепутаны, чтобы не злоупотребляли!
AV
Я кстати не понимаю практический смысл того, что язык не turing complete и программы завершаемы
JS
Да, операнды перепутаны, чтобы не злоупотребляли!
не перепутаны, это «вычесть _ из _» как в Хаскеле, для каррирования
(subtract 3) вычитает 3
(subtract 3) вычитает 3
PS
Я кстати не понимаю практический смысл того, что язык не turing complete и программы завершаемы
"Вы же не хотите, чтобы Ваша конфигурация попала в бесконечный цикл?"
AV
Да! Я хочу, чтобы она вычисляла конечный цикл время сравнимое со временем жизни вселенной! Ведь это большая разница!
AV
Да что там, вычисление в течении часа зачастую неотличимо от бесконечного цикла
JS
Я кстати не понимаю практический смысл того, что язык не turing complete и программы завершаемы
это же для конфигов. запретить писать сложные конфиги, но разрешить абстрагироваться