Effect system

Last updated

In computing, an effect system is a formal system that 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.

Contents

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 (parameters) 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 (for example, a type of a mutable memory cell is parameterized by the label of the memory region in which the cell resides). The term "algebraic effect" follows from the type system.

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]

Examples

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). [2]

Implementations

Core feature

Full support

Partial support and prototypes

References

  1. Turbak, Franklyn Albin; Gifford, David K.; Sheldon, Mark A. (2010). Design concepts in programming languages. PHI Learning. ISBN   978-81-203-3996-5. OCLC   1261053520.
  2. Abramov, Dan (21 July 2019). "Algebraic Effects for the Rest of Us". overreacted.io. Retrieved 20 August 2025.
  3. Leijen, Daan (22 July 2025). "The Koka Programming Language". koka-lang.github.io. Archived from the original on 26 July 2025. Retrieved 20 August 2025.
  4. Pretnar, Matija, "Eff", Github, retrieved 11 December 2021
  5. "Eff programming language". eff-lang.org. Retrieved 20 August 2025.
  6. "The Unison language". www.unisonweb.org. Archived from the original on 5 December 2021. Retrieved 7 December 2021.
  7. The Effekt research team. "Effekt Language: Concepts and Features". Effekt Language. Retrieved 13 June 2023.
  8. Vera, Josh (18 April 2020). "freemonad benchmark". GitHub. A benchmark comparing the performance of different free monad implementations.
  9. E. Moggi and Amr Sabry. 2001. Monadic Encapsulation of Effects: A Revised Approach (Extended Version). J. Funct. Program. 11, 6 (Nov. 2001), 591-627
  10. "Chapter 12 Language extensions". v2.ocaml.org. Archived from the original on 13 June 2023. Retrieved 13 June 2023.
  11. "CanThrow Abilities". Scala Documentation. Retrieved 7 December 2021.
  12. Pulley, Rocky (12 August 2013). "Java 8 Lambda function that throws exception?". Stack Overflow. Retrieved 25 December 2021.

Textbook chapters

Overview papers

Further reading