SA
ну да
Да
Повторю, как я понял (а то вдруг тож неверно интерпретирую)
Есть правила для монад:
return a >>= f = f a
m >>= return = m
...
Size: a a a
2020 August 26
χλ
Компилятор их не проверяет, но делает оптимизацию, будто бы они выполняются
PG
нооо будут другие проблемы
да, например отсутствие полноты по Тьюрингу
SA
мм погоди но когда ты пишешь свою херню ты ж должен там их написать
SA
и мне кажется он не давал
SA
не писать
χλ
Чего?
SA
return/»=
χλ
Хаскел никаким образом не способен проверить выполнение правил монадных
χλ
return/»=
Ты должен им определение дать
χλ
Да
Повторю, как я понял (а то вдруг тож неверно интерпретирую)
Есть правила для монад:
return a >>= f = f a
m >>= return = m
...
Повторю, как я понял (а то вдруг тож неверно интерпретирую)
Есть правила для монад:
return a >>= f = f a
m >>= return = m
...
А тут уравнения _)
SA
нуу по типам он может проверить
SA
а про то что оно всегда будет работать так как надо
SA
там где ты ее пишешь?
SA
ну блин да
SA
естественно)
χλ
Ну да
SA
лан соре мы про разное говорили
V(
По хорошему должно быть как в https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Interfaces/Verified.idr
вот с эта штука у меня в шортлисте