Effect laws are undocumented

[robrix]

Effects typically have laws which carriers should observe. e.g., given a Reader effect, sequential asks in the same do-block are expected to return the same value (whereas a carrier for e.g. Reader Int could be implemented to store and increment the value before returning). Unfortunately, these are currently undocumented, which makes it harder to know that your carrier is (in addition to type-checking) correct.

NB: Some of these might be somewhat subtle when considering interactions between effects; e.g. State inside NonDet is maintained per-branch, whereas State outside NonDet is global. This is a feature, in general, since it allows you to select the desired composite semantics by reordering, but it may make it harder to state some of the laws succinctly.

For example, it’s tempting to say that ask >>= \ before -> m >> ask >>= \ after -> pure (before == after) should (observationally) equal pure True for arbitrary m, but if m doesn’t continue (e.g. because it contains a throwError, fail, or empty), that is not strictly true.