1. буллшит
2. хз вроде збс
3. бля десять лет джу
4. линзы в пизду ура
5. похуй
6. хз даж надо попробовать
7. хз никогда свои числа не хотелось ещё написать
8. заебись
9. че блядь?!
10. чёт хз яннп надо смотреть конкретные примеры
CONCLUSION: хз даж надо попробовать
Idris provides a library, Effects [3], which captures this pattern and many others involving effectful computation [1]. An effectful program f has a type of the following form:
f : (x1 : a1) -> (x2 : a2) -> ... -> Eff t effs
That is, the return type gives the effects that f supports (effs, of type List EFFECT) and the type the computation returns t.
@l29ah > 9. че блядь?!
вычисление функции не вызывает сайд-эффектов, ее выполнение - вызываает.
@l29ah http://docs.idris-lang.org/en/latest/effects/state.html#introducing-effects
Idris provides a library, Effects [3], which captures this pattern and many others involving effectful computation [1]. An effectful program f has a type of the following form:
f : (x1 : a1) -> (x2 : a2) -> ... -> Eff t effs
That is, the return type gives the effects that f supports (effs, of type List EFFECT) and the type the computation returns t.