gluon icon indicating copy to clipboard operation
gluon copied to clipboard

Improve effect documentation

Open LordMZTE opened this issue 4 years ago • 1 comments

Currently, to a newcomer the documentation on effects in the book might be a little confusing. Here's some things I think could do with some improvement:

  • make it clear that the name of effects in the effect row is important
  • explain a little of how the get, put and modify actions work internally and how they access the state effect
  • explain what the Eff type is and how it's declared, and in the Embedding API chapter explain what this kind of type is good for and how to add it to a project
  • add some more in-depth explanation to what lift does
  • what do the run_lift and eval_state functions do so they're able to be chained as in the guessing game example, and how can effects be run sequentially like this?

LordMZTE avatar Oct 01 '21 18:10 LordMZTE

Hey I would be willing to work on this. I would like to know exactly how effects are implemented? Using monads, a la Haskell? Algebraic effects a la Eff? Non-well-founded trees as in the ooAgda library? Also, it would be a great help if you could point me to where the code for effects is.

rahulc29 avatar Jul 21 '23 09:07 rahulc29