DS
Чёрт знает как оно в реальности в идрисе сработает, но почему бы и нет.
Size: a a a
2020 August 17
DS
Мне в этом плане нравится разделение на языки которые больше пруверы и языки, которые больше general purpose. Идрис всё же ко второму тяготеет очень сильно.
DS
И раз это не прувер, то почему бы не заюзать весь фан его типов, даже если это может привести к странным результатам
p
что пофигу? Я не вижу зачем на тайплевеле нетотальные функции иметь
+, не надо так делаиь
p
Чёрт знает как оно в реальности в идрисе сработает, но почему бы и нет.
Тебе придется IO Type возвращать, что выглядит странно
AZ
Тебе придется IO Type возвращать, что выглядит странно
не надо если сделать ансейфперформ или другую гадость
p
не надо если сделать ансейфперформ или другую гадость
Но зачем
AZ
ну типа во время комплияции например схему как дизель компилить
AZ
но чтобы ты не с помощью CLI собирал а чтобы он во врем ясборки сам в БД сходил и схему подсмотрел
AZ
хз, мне такое не нравится но доге вот любит
DS
хз, мне такое не нравится но доге вот любит
Оно мне нравится, если оно норм работает в плане UX
DS
И есть вероятность, что вариант с этим в зав типах будет работать лучше, чем с макросами в этом плане
AZ
мне не нравится вариант когда ты не можешь скомпилировать сорцы без интернета
AZ
теряется повторяемость сборки
Т8
мне не нравится вариант когда ты не можешь скомпилировать сорцы без интернета
Ты пробовал собирать проект с крейтами без интернета?
AZ
так и знал что ты до этого доебешься))
AZ
надо в ванги идти
Т8
Меня карго посылал на хуй
AZ
вопрос не в том что нет интернета
AZ
а когда у тебя сборка может успешно/неуспешно выполниться от фазы луны