KV
Не, Ваш подход означает повсеместные доказательства, а более простой нет
1 как без доказательства сделать гарантированно завершаемую функцию
2 такой язык не будет полным по Тьюрингу
Size: a a a
2021 May 29
KV
Функция, которая не завершается, ничё не возвращает, в том числе боттом значение, не понимаю, что это за прикол вообще такой
[
Функция, которая не завершается это боттом значение - скажет мне любой гайд по хаскелю, гле объясняется суть боттом
KV
Там ещё могут написать, что Hask — это категория
JS
да, пишут сервера и интерактивные приложения
JS
1 использовать только конечные примитивы. например, списки — только конечные, циклы — только по списку
[
И много таким языком выразишь?
JS
вечно работающие процедуры с эффектами полезны
JS
смарт-контракты примерно на таких пишут
KV
Не спорю, но они ж ничего не возвращают
JS
то есть да, много
JS
да. не возвращают и полезны. здорово же
KV
Ну вот, а говорят, что возвращают какое-то _|_
JS
это то же самое. не завершаться по-настоящему — это как бы вычисляться в дно
KV
Ну типа
[
Кстати! Я тут подумал и пришёл к мысли, что мой подход на доказательствах без нормальных завтипов нормально не работает
JS
в языке типов GHC можно почти всё, но он завершается, потому что счётчик итераций обрубает