p
Он более ебнутый
Size: a a a
2021 May 29
gо
Во-первых, тогда у тебя чистый язык
gо
Если у тебя не чистый язык с вычислениями на тайп-левеле, то ты в жопе
p
Ну это очевидно
gо
Чистый язык => сложный рантайм
p
Там же в примере был IO
H
либо компилируешь тайплевел jit'ом
p
Эм?
p
Где
gо
И чо? Тебя это как-то спасёт от
rand() на тайплевелеgо
Кто-то у тебя IO-монаду должен обратно разворачивать и выполнять
gо
Фиг бы с этим
p
Я не говорил что буду честно разворачивать и выполнять что-то
gо
Если у тебя чистый язык с произвольными вычислениями на тайп-левеле, то тебе вообще не нужна система пруфов
p
Ну и да, чистота и прочее это фигня которая будет потом
p
Мне гораздо интереснее проверить эту концепцию с пруфами без пруфов
p
Почему
gо
Зачем? Рефайнишь тип и пишешь код, который для рефайнед типов проверяет утверждения
gо
Прямо в стдлибе и пишешь
gо
У тебя есть
Refined(int, Lt(20)) и тебе нужен Refined(int, Lt(15)). Осталось реализовать From<Lt<N>> for Lt<M> where N < M и всё.