<p>I struggle to get the thing about &quot;algebraic effect systems&quot;. What is it really about? Is it mostly about that functions doing IO (e.g. http request) should have that IO-operation visible in the type signature? Is that like in Elm where http-requests, has a <code>Cmd</code> in its types? see e.g. <a href="https://github.com/elm/http" rel="noreferrer">elm http module</a>:</p>
<pre><code>getBook : Cmd Msg
getBook =
  Http.get
    { url = &quot;https://elm-lang.org/assets/public-opinion.txt&quot;
    , expect = Http.expectString GotBook
    }
</code></pre>
<p>But also, many languages now use <em>async-await</em> for IO, so is that also an implementation of a &quot;effect system&quot;? JavaScript function signature:</p>
<pre><code>async function fetchPokemon(name)
</code></pre>
<p>I cannot really get a clear understanding. If you can do IO without showing it in the type signature, does that mean that the language does not have an &quot;effect system&quot;?</p>

<types><async><effect-systems>
What does it mean that a language has an "effect system"?
CC BY-SA 4.0
2024-04-24T15:13:55.570Z
It's always tricky to answer a question about a misunderstanding because it is hard to know what false belief you have. Let me ask a few clarifying questions: what are "type systems" really about? Does JavaScript have a "type system"? Does any language that lacks "type signatures" have a type system? Knowing what you understand (or misunderstand) about type systems will inform how to write a good answer to this question.
Eric Lippert
CC BY-SA 4.0
2024-04-24T15:20:35.253Z
@EricLippert sure, I see "type systems" as a way to define "constraints" that can be verified, e.g. to avoid mistakes. JavaScript does have Types, but not a static type system, as how I see it, although the example I wrote can also be applicable for e.g. TypeScript that has a Type System. I am only a developer, so I don't have academic insight in the correct terminology, I apologize for that.
Jonas
CC BY-SA 4.0
2024-04-24T15:23:46.667Z
No need to apologize, that's helpful for understanding where you're at. (And there's no need to use a pejorative "only"! You're a developer who does not *yet* have academic insights. You can cultivate those insights, lots of developers do!)
Eric Lippert
<p>There is no agreed-on definition of effect, but as a first approximation, we might approach the concept of effect  as one of:</p>
<ul>
<li>Something that might break referential transparency.</li>
<li>Effects as instances of interacting with a global coordinator, such as global state or an operating system kernel.</li>
</ul>
<p>The latter comes from [1] where we find quotes like <em>&quot;An effect is most easily understood as an interaction between a sub-expression
and a central authority that administers the global resources of a program. 4 Examples of such resources are stores, heaps, file systems, the place for the final
result of a program, and other input/output channels. Given an administrator,
an effect can be viewed as a message to the central authority plus enough information to resume the suspended calculation.&quot;</em></p>
<p>Effect <em>systems</em> are features of typing systems that make guarantees about what effects a program fragment does or does not have. For example the parameters a system call to the OS is expecting, or, if the effect system has linearity, if a system call is guaranteed to return. A classic example is purity, which indicates that code does not have any effects. Those guarantees are useful for reasoning about correctness and enable compiler optimisations. (Note that an optimising compiler infers information about programs that can be seen as effects, even if the source language has no effects.)</p>
<p>So <strong>effects themselves can be understood without reference to types</strong>. (This is not saying much, because  machine language is always untyped, so any program will eventually be executed in an untyped manner.) Effect <strong>systems</strong> are features of typing systems that make guarantees about what effects a program fragment does or does not have. For example: what are  the parameters a system call to the OS is expecting? or:  if a system call is guaranteed to return. Finally, a classic example is purity, which indicates that code does not have any effects. Those guarantees are useful for reasoning about correctness and enable compiler optimisations. (Note that an optimising compiler infers information about programs that can be seen as effects, even if the source language has no effects.)</p>
<p><strong>Summary.</strong>  Effects are a form of (well-behaved) non-local computation, and effect systems help to constrain this non-local computation.</p>
<hr>
<ol>
<li>R. Cartwright, M. Felleisen, <em>Extensible Denotational Language Specifications.</em></li>
</ol>

CC BY-SA 4.0
2024-05-23T17:47:44.033Z
2024-05-24T10:41:42.650Z
2024-05-24T10:41:42.650Z
Martin Berger
CC BY-SA 4.0
2024-05-23T22:28:07.643Z
However, this only explains what an "effect" is, and not so much about an "effect system for a language".
Jonas
CC BY-SA 4.0
2024-05-24T09:34:01.260Z
@Jonas Good point, I've added some notes.
Martin Berger
<blockquote>
<p>I struggle to get the thing about &quot;algebraic effect systems&quot;. What is it really about?</p>
</blockquote>
<p>Since you're not asking for a formal definition, but rather saying that you don't intuitively grasp the concept at all, I'm going to avoid formalisms in this answer and be a little hand wavy throughout.</p>
<p>Let's take a few steps back.</p>
<p>A language specification often divides up the data manipulated by the program into various &quot;types&quot;. A &quot;type system&quot; describes those types and, importantly, what the rules of the language are for determining the types of variables, expressions, and so on.</p>
<p>For example, JavaScript has a comparatively simple type system with less than a dozen types, but very complicated rules for how you deduce the type of an expression. If I tell you that you have an expression <code>x + y</code> and give you the values of <code>x</code> and <code>y</code>, then you can get out the spec, look up the addition operator, follow the rules, and you can logically deduce what the type of <code>x + y</code> will be.</p>
<p>That's really all a type system is: a bunch of rules that give you a way to analyze a language.</p>
<p><em>Some</em> languages have <em>many</em> more than a dozen types; many languages allow developers to define new types or combine existing types. And many languages  allow/require the developer to put &quot;type annotations&quot; in their programs -- typically on variable declarations and method declarations -- so that a compiler can (1) analyze the program for violations of desirable type safety properties, and (2) generate more efficient code out the back end.</p>
<p>The distinction that I'm making here is important for your understanding. A type system is a bunch of rules for how types work, irrespective of whether the language requires type annotations, and irrespective of whether the language is strict or lax in its pursuit of preventing type errors. JavaScript has a type system, even without type annotations, even without strict rules for what kinds of data you can assign to a variable or what operations you can perform.</p>
<p>With that background we can very simply say what an &quot;effect system&quot; is.</p>
<p>Evaluating an expression potentially does two things: produces a <em>value</em> and produces an <em>effect</em>.  (In many languages an evaluation can do a third thing: produce an <em>exception</em>, but let's ignore that for the purposes of this discussion; this gets us into effect handlers and other more advanced topics.) Examples of effects are &quot;write to an array&quot; or &quot;allocate a new block of memory&quot;.</p>
<p>We've said that the type system of the language is a list of rules for logically determining the type of the value produced by an expression if you know the types of the operands. The &quot;effect system&quot; is simply the rules for logically determining the side effects of an expression and where those effects are visible.</p>
<p>Many languages require the developer to put type annotations in a program so that it can be analyzed -- type signatures on method declarations, for instance -- but most do not have any way to put &quot;effect annotations&quot; on regions of code.</p>
<p>But that's all that an effect system is: a bunch of rules for logically deducing what effect a particular expression will have when evaluated, and where that effect is visible in the program.</p>
<p>Just as with type annotations, a language designer could make &quot;effect annotations&quot; impossible, optional or required. And the compiler writer can use those rules to (1) look for violations of safety rules in a program and (2) generate more efficient code.</p>
<p>Mainstream languages typically do not have effect annotations; some have the simplest possible effect annotation &quot;pure&quot;, meaning &quot;this method has no effects that are visible from outside the body of the method and observes no effects from outside either&quot;.</p>
<p>Think about what an optimizing compiler can do if it knows a method is pure. For safety: a pure method that calls an impure method likely has a bug. For performance, there's lots you can do. A call to a pure method whose returned value is never used can be elided safely.  A compiler can automatically memoize pure methods. If the method is called in a loop then that loop can be parallelized to many threads safely. And so on. Even the simplest possible effects analysis can lead to big wins.</p>
<blockquote>
<p>Is it mostly about functions doing IO should have that IO-operation visible in the type signature?</p>
</blockquote>
<p>I/O is a great example of an effect that could be tracked by an effect system. Whether a language <em>requires</em> that you annotate your I/O effects or not is up to the language designer.</p>
<blockquote>
<p>many languages now use async-await for IO, so is that also an implementation of a &quot;effect system&quot;?</p>
</blockquote>
<p>Not really. Asynchronous workflows are workflows where methods can return control to their caller before their work is complete, and resume where they left off later. Languages with asynchronous workflows make it harder to do an effects analysis because you can no longer rely on the invariant that all the effects of a method will happen before it returns control! But async workflows themselves are not an example of an effect system. (Asynchronous workflows, like exceptions, can be <em>implemented</em> via effect handlers, but again, I'm not going to get into that in this brief introduction to effect systems.)</p>
<blockquote>
<p>If you can do IO without showing it in the type signature, does that mean that the language does not have an &quot;effect system&quot;?</p>
</blockquote>
<p>No. Just as a language specification can describe how to do type analysis without requiring type annotations, a language specification can also describe how to analyze the visibility of side effects without having effect annotations. The C# spec, for example, gives rules for how the effects of reading and writing volatile variables may and may not be observed to be ordered, but has no way in the language of indicating what effect a method has.</p>
<p>I hope that answers your question; I note that I did not actually give an example of a simple effect system or say <em>specifically</em> what effects are useful to track. I suspect you have not read the original papers on effect systems and I recommend that you do, to delve into this topic a little deeper.</p>
<p><a href="https://dl.acm.org/doi/pdf/10.1145/319838.319848" rel="noreferrer">https://dl.acm.org/doi/pdf/10.1145/319838.319848</a></p>
<p><a href="https://groups.csail.mit.edu/pag/OLD/parg/lucassen88effects.pdf" rel="noreferrer">https://groups.csail.mit.edu/pag/OLD/parg/lucassen88effects.pdf</a></p>

CC BY-SA 4.0
2024-04-24T16:02:03.013Z
2024-04-26T03:06:48.787Z
2024-04-26T03:06:48.787Z
Eric Lippert
CC BY-SA 4.0
2024-04-24T20:03:01.613Z
Woof those refs are old. Here's one from this century: https://arxiv.org/abs/1306.6316
cody
CC BY-SA 4.0
2024-04-24T21:49:41.500Z
@cody: They are the original papers describing the idea by the people who invented it; I always like to go back to the originals when I'm trying to understand a thing.
Eric Lippert
CC BY-SA 4.0
2024-04-25T11:42:31.460Z
(I know little of effect systems) -- I find it strange that you describe "exceptions" as a 3rd thing on top of types & effects, when in many discussions about effect systems, I've seen exceptions referred to as an effect (one form of a diverging effect).
Matthieu M.
CC BY-SA 4.0
2024-04-25T13:31:21.203Z
Could you provide some examples of languages that do have effect annotations? The idea sounds great, but I'm curious now on what the *effect* is on aesthetics and verbosity in some of the common implementations.
JBraha
CC BY-SA 4.0
2024-04-25T14:37:00.273Z
@JBraha Koka seems to be such a language: https://koka-lang.github.io/koka/doc/book.html
Jonas
CC BY-SA 4.0
2024-04-25T16:58:25.533Z
"you can no longer rely on the invariant that all the effects of a method will happen before it returns control" you probably couldn't unconditionally rely on that anyway, as some of the method's effects may be used only within a specific branch or if statement, etc. I might rather say control being returned from an asynchronous method doesn't mean that it has finished.
Dev
CC BY-SA 4.0
2024-04-25T17:59:42.890Z
@MatthieuM. Both exceptions and async/await can be implemented or modeled or typed as/using effects, but I think it's probably fair to say that a language can implement them on their own *without* effects, in the same sense as e.g. a language implementing structured control flow without exposing `goto`.
rpjohnst
CC BY-SA 4.0
2024-04-25T18:13:37.270Z
@EricLippert that's fair, though sometimes things gain clarity with time (and notations and language evolves, of course).
cody
CC BY-SA 4.0
2024-04-25T18:17:40.143Z
@MatthieuM. that's right, but the connection between effects and non-local control flows such as exceptions is the sort of thing I'm trying to not worry about in what is intended to be a brief introduction for someone who lacks an intuitive understanding of the concept. I didn't want this answer to over-explain.
Eric Lippert
CC BY-SA 4.0
2024-04-25T18:24:11.597Z
@MatthieuM.: I'll update the text to make this more clear.
Eric Lippert
CC BY-SA 4.0
2024-04-25T20:26:58.047Z
Is the `const` keyword in C/C++ an example of a rudimentary effect notation?
Charles Staats
CC BY-SA 4.0
2024-04-25T23:18:03.123Z
@CharlesStaats: Yes, that's a good point. If we have `void foo(const T &x)` then we have a restriction on effects: the object referred to by x cannot be modified by foo via the alias x. (As I occasionally point out, that is not the statement "The  object referred to by x has the same state after foo returns as before it runs", which would be a stronger and more useful restriction.)  But as a rule describing restrictions on effects, we can think of it as part of the effect system of C++.
Eric Lippert
# What does it mean that a language has an "effect system"?
Posted by: username_0 on 2024-04-24
I struggle to get the thing about "algebraic effect systems". What is it really about? Is it mostly about that functions doing IO (e.g. http request) should have that IO-operation visible in the type signature? Is that like in Elm where http-requests, has a Cmd in its types? see e.g. elm http module:
getBook : Cmd Msg
getBook =
  Http.get
    { url = "https://elm-lang.org/assets/public-opinion.txt"
    , expect = Http.expectString GotBook
    }

But also, many languages now use async-await for IO, so is that also an implementation of a "effect system"? JavaScript function signature:
async function fetchPokemon(name)

I cannot really get a clear understanding. If you can do IO without showing it in the type signature, does that mean that the language does not have an "effect system"?
**Tags:** types async effect-systems
> **Comments:**
> **username_1**: It's always tricky to answer a question about a misunderstanding because it is hard to know what false belief you have. Let me ask a few clarifying questions: what are "type systems" really about? Does JavaScript have a "type system"? Does any language that lacks "type signatures" have a type system? Knowing what you understand (or misunderstand) about type systems will inform how to write a good answer to this question.  
> **username_0**: @EricLippert sure, I see "type systems" as a way to define "constraints" that can be verified, e.g. to avoid mistakes. JavaScript does have Types, but not a static type system, as how I see it, although the example I wrote can also be applicable for e.g. TypeScript that has a Type System. I am only a developer, so I don't have academic insight in the correct terminology, I apologize for that.  
> **username_1**: No need to apologize, that's helpful for understanding where you're at. (And there's no need to use a pejorative "only"! You're a developer who does not *yet* have academic insights. You can cultivate those insights, lots of developers do!)  
---
## 2 answers
### Answer by username_1 on 2024-04-24. Score: 30 | Accepted answer
> I struggle to get the thing about "algebraic effect systems". What is it really about?

Since you're not asking for a formal definition, but rather saying that you don't intuitively grasp the concept at all, I'm going to avoid formalisms in this answer and be a little hand wavy throughout.

Let's take a few steps back.

A language specification often divides up the data manipulated by the program into various "types". A "type system" describes those types and, importantly, what the rules of the language are for determining the types of variables, expressions, and so on.

For example, JavaScript has a comparatively simple type system with less than a dozen types, but very complicated rules for how you deduce the type of an expression. If I tell you that you have an expression `x + y` and give you the values of `x` and `y`, then you can get out the spec, look up the addition operator, follow the rules, and you can logically deduce what the type of `x + y` will be.

That's really all a type system is: a bunch of rules that give you a way to analyze a language.

*Some* languages have *many* more than a dozen types; many languages allow developers to define new types or combine existing types. And many languages allow/require the developer to put "type annotations" in their programs -- typically on variable declarations and method declarations -- so that a compiler can (1) analyze the program for violations of desirable type safety properties, and (2) generate more efficient code out the back end.

The distinction that I'm making here is important for your understanding. A type system is a bunch of rules for how types work, irrespective of whether the language requires type annotations, and irrespective of whether the language is strict or lax in its pursuit of preventing type errors. JavaScript has a type system, even without type annotations, even without strict rules for what kinds of data you can assign to a variable or what operations you can perform.

With that background we can very simply say what an "effect system" is.

Evaluating an expression potentially does two things: produces a *value* and produces an *effect*. (In many languages an evaluation can do a third thing: produce an *exception*, but let's ignore that for the purposes of this discussion; this gets us into effect handlers and other more advanced topics.) Examples of effects are "write to an array" or "allocate a new block of memory".

We've said that the type system of the language is a list of rules for logically determining the type of the value produced by an expression if you know the types of the operands. The "effect system" is simply the rules for logically determining the side effects of an expression and where those effects are visible.

Many languages require the developer to put type annotations in a program so that it can be analyzed -- type signatures on method declarations, for instance -- but most do not have any way to put "effect annotations" on regions of code.

But that's all that an effect system is: a bunch of rules for logically deducing what effect a particular expression will have when evaluated, and where that effect is visible in the program.

Just as with type annotations, a language designer could make "effect annotations" impossible, optional or required. And the compiler writer can use those rules to (1) look for violations of safety rules in a program and (2) generate more efficient code.

Mainstream languages typically do not have effect annotations; some have the simplest possible effect annotation "pure", meaning "this method has no effects that are visible from outside the body of the method and observes no effects from outside either".

Think about what an optimizing compiler can do if it knows a method is pure. For safety: a pure method that calls an impure method likely has a bug. For performance, there's lots you can do. A call to a pure method whose returned value is never used can be elided safely. A compiler can automatically memoize pure methods. If the method is called in a loop then that loop can be parallelized to many threads safely. And so on. Even the simplest possible effects analysis can lead to big wins.

> Is it mostly about functions doing IO should have that IO-operation visible in the type signature?

I/O is a great example of an effect that could be tracked by an effect system. Whether a language *requires* that you annotate your I/O effects or not is up to the language designer.

> many languages now use async-await for IO, so is that also an implementation of a "effect system"?

Not really. Asynchronous workflows are workflows where methods can return control to their caller before their work is complete, and resume where they left off later. Languages with asynchronous workflows make it harder to do an effects analysis because you can no longer rely on the invariant that all the effects of a method will happen before it returns control! But async workflows themselves are not an example of an effect system. (Asynchronous workflows, like exceptions, can be *implemented* via effect handlers, but again, I'm not going to get into that in this brief introduction to effect systems.)

> If you can do IO without showing it in the type signature, does that mean that the language does not have an "effect system"?

No. Just as a language specification can describe how to do type analysis without requiring type annotations, a language specification can also describe how to analyze the visibility of side effects without having effect annotations. The C# spec, for example, gives rules for how the effects of reading and writing volatile variables may and may not be observed to be ordered, but has no way in the language of indicating what effect a method has.

I hope that answers your question; I note that I did not actually give an example of a simple effect system or say *specifically* what effects are useful to track. I suspect you have not read the original papers on effect systems and I recommend that you do, to delve into this topic a little deeper.

<https://dl.acm.org/doi/pdf/10.1145/319838.319848>

<https://groups.csail.mit.edu/pag/OLD/parg/lucassen88effects.pdf>
> **Comments:**
> **username_3** (2024-04-24): Woof those refs are old. Here's one from this century: https://arxiv.org/abs/1306.6316  
> **username_1** (2024-04-24): @cody: They are the original papers describing the idea by the people who invented it; I always like to go back to the originals when I'm trying to understand a thing.  
> **username_4** (2024-04-25): (I know little of effect systems) -- I find it strange that you describe "exceptions" as a 3rd thing on top of types & effects, when in many discussions about effect systems, I've seen exceptions referred to as an effect (one form of a diverging effect).  
> **username_5** (2024-04-25): Could you provide some examples of languages that do have effect annotations? The idea sounds great, but I'm curious now on what the *effect* is on aesthetics and verbosity in some of the common implementations.  
> **username_0** (2024-04-25): @JBraha Koka seems to be such a language: https://koka-lang.github.io/koka/doc/book.html  
> **username_6** (2024-04-25): "you can no longer rely on the invariant that all the effects of a method will happen before it returns control" you probably couldn't unconditionally rely on that anyway, as some of the method's effects may be used only within a specific branch or if statement, etc. I might rather say control being returned from an asynchronous method doesn't mean that it has finished.  
> **username_7** (2024-04-25): @MatthieuM. Both exceptions and async/await can be implemented or modeled or typed as/using effects, but I think it's probably fair to say that a language can implement them on their own *without* effects, in the same sense as e.g. a language implementing structured control flow without exposing `goto`.  
> **username_3** (2024-04-25): @EricLippert that's fair, though sometimes things gain clarity with time (and notations and language evolves, of course).  
> **username_1** (2024-04-25): @MatthieuM. that's right, but the connection between effects and non-local control flows such as exceptions is the sort of thing I'm trying to not worry about in what is intended to be a brief introduction for someone who lacks an intuitive understanding of the concept. I didn't want this answer to over-explain.  
> **username_1** (2024-04-25): @MatthieuM.: I'll update the text to make this more clear.  
> **username_8** (2024-04-25): Is the `const` keyword in C/C++ an example of a rudimentary effect notation?  
> **username_1** (2024-04-25): @CharlesStaats: Yes, that's a good point. If we have `void foo(const T &x)` then we have a restriction on effects: the object referred to by x cannot be modified by foo via the alias x. (As I occasionally point out, that is not the statement "The  object referred to by x has the same state after foo returns as before it runs", which would be a stronger and more useful restriction.)  But as a rule describing restrictions on effects, we can think of it as part of the effect system of C++.  
---
### Answer by username_2 on 2024-05-23. Score: 2
There is no agreed-on definition of effect, but as a first approximation, we might approach the concept of effect as one of:

* Something that might break referential transparency.
* Effects as instances of interacting with a global coordinator, such as global state or an operating system kernel.

The latter comes from [1] where we find quotes like *"An effect is most easily understood as an interaction between a sub-expression
and a central authority that administers the global resources of a program. 4 Examples of such resources are stores, heaps, file systems, the place for the final
result of a program, and other input/output channels. Given an administrator,
an effect can be viewed as a message to the central authority plus enough information to resume the suspended calculation."*

Effect *systems* are features of typing systems that make guarantees about what effects a program fragment does or does not have. For example the parameters a system call to the OS is expecting, or, if the effect system has linearity, if a system call is guaranteed to return. A classic example is purity, which indicates that code does not have any effects. Those guarantees are useful for reasoning about correctness and enable compiler optimisations. (Note that an optimising compiler infers information about programs that can be seen as effects, even if the source language has no effects.)

So **effects themselves can be understood without reference to types**. (This is not saying much, because machine language is always untyped, so any program will eventually be executed in an untyped manner.) Effect **systems** are features of typing systems that make guarantees about what effects a program fragment does or does not have. For example: what are the parameters a system call to the OS is expecting? or: if a system call is guaranteed to return. Finally, a classic example is purity, which indicates that code does not have any effects. Those guarantees are useful for reasoning about correctness and enable compiler optimisations. (Note that an optimising compiler infers information about programs that can be seen as effects, even if the source language has no effects.)

**Summary.** Effects are a form of (well-behaved) non-local computation, and effect systems help to constrain this non-local computation.

---

1. R. Cartwright, M. Felleisen, *Extensible Denotational Language Specifications.*
> **Comments:**
> **username_0** (2024-05-23): However, this only explains what an "effect" is, and not so much about an "effect system for a language".  
> **username_2** (2024-05-24): @Jonas Good point, I've added some notes.  
---
