АГ
Идрис тотальный
Size: a a a
2021 May 31
АГ
Хаскель даже не безопасный, как его любят продавать. Вообще ужасный язык, едва там все работает
˸A
😳 впервые слышу такой отзыв о Хаскеле. Всегда именно его рекомендовали, как лучший ФП ЯП
П. С. К идрису давно присматриваюсь... жаль, его популярность - ещё меньше хаскеля...
П. С. К идрису давно присматриваюсь... жаль, его популярность - ещё меньше хаскеля...
АГ
Ну а где это видано, чтобы исключения из всех щелей летели. А в Хаскеле летят.
DG
А коданные это в том значении, в котором они вот тут описаны?
https://www.cs.uoregon.edu/Reports/MS-201806-Sullivan.pdf
https://www.cs.uoregon.edu/Reports/MS-201806-Sullivan.pdf
АГ
А еще просто писать на Хаскеле нельзя, нужно кучу патчей в компиляторе включать, чтобы хоть что-то работало
DG
Это у тебя такое чувство юмора или ты абсолютно серьёзно это утвержаешь?
АГ
У меня новое измерение - серьезное чувство юмора
DG
😂👍
˸A
вроде да (судя по второй главе)
и да, я согласен, что в некоторых частных случаях можно из кодаты вывести дату (биекция на эндофункторах)
и да, я согласен, что в некоторых частных случаях можно из кодаты вывести дату (биекция на эндофункторах)
AG
от языка зависит, обычно трейты вводятся для множественного наследования и имеют какие-то доп ограничения, позволяющие избегать алмазов
AG
idris/agda/coq, из не-зависимых dhall например
2021 June 01
AG
одновременно это вот как раз в хаскеле например, если есть различение на уровне языка (конструкторы vs деструкторы) то по определению не могут быть одновременно
AG
в целом данные обычно можно упаковать в коданные и это будет по сути инкапсуляция - мы забываем как что-то построено, но говорим как оно может быть разобрано через некоторое апи
˸A
Ок. Не компетентен в хаскеле. Но смысл такого ограничения?
˸A
Стоп. Тут речь о разных датах шла (хотя есть паттерны, которые в кодате конструируют дату того же типа)
AG
да, как вариант
AG
как и для любого типа - строгость
AG
Either Int String и (b : Bool ** if b then Int else String) тоже очень похожи, но это разные типы˸A
Это же обычный карри: задаём первый параметр - и получаем дату для конструирования новой кодаты (чаще всего другой, чем оригинальная - placeOrder -> invoice -> invoice codata)