Effect system


In computing, an effect system is a formal system which describes the computational effects of computer programs, such as side effects. An effect system can be used to provide a compile-time check of the possible effects of the program.
The effect system extends the notion of type to have an "effect" component, which comprises an effect kind and a region. The effect kind describes what is being done, and the region describes with what it is being done.
An effect system is typically an extension of a type system. The term "type and effect system" is sometimes used in this case. Often, a type of a value is denoted together with its effect as type ! effect, where both the type component and the effect component mention certain regions.
Some examples of the behaviors that can be described by effect systems include:
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.

Textbook chapters

Overview papers

*