effect, where both the type component and the effect component mention certain regions (for example, a type of a mutable memory cell is parameterized by the label of the memory region in which the cell resides).
Effect systems may be used to prove the external purity of certain internally impure definitions: for example, if a function internally allocates and modifies a region of memory, but the function's type does not mention the region, then the corresponding effect may be erased from the function's effect.
[1] Some examples of the behaviors that can be described by effect systems include: From a programmer's point of view, effects are useful as it allows for separating the implementation (how) of specific actions from the specification of what actions to perform.
For example, an ask name effect can read from either the console, pop a window, or just return a default value.
The control flow can be described as a blend of yield (in that the execution continues) and throw (in that an unhandled effect propagates down until handled).