17
$\begingroup$

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"?

$\endgroup$
3
  • 2
    $\begingroup$ 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. $\endgroup$ Apr 24 at 15:13
  • 1
    $\begingroup$ @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. $\endgroup$
    – Jonas
    Apr 24 at 15:20
  • 3
    $\begingroup$ 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!) $\endgroup$ Apr 24 at 15:23

2 Answers 2

30
$\begingroup$

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

$\endgroup$
12
  • 9
    $\begingroup$ @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. $\endgroup$ Apr 24 at 21:49
  • 2
    $\begingroup$ (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). $\endgroup$ Apr 25 at 11:42
  • 2
    $\begingroup$ @JBraha Koka seems to be such a language: koka-lang.github.io/koka/doc/book.html $\endgroup$
    – Jonas
    Apr 25 at 14:37
  • 3
    $\begingroup$ @EricLippert that's fair, though sometimes things gain clarity with time (and notations and language evolves, of course). $\endgroup$
    – cody
    Apr 25 at 18:13
  • 5
    $\begingroup$ @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++. $\endgroup$ Apr 25 at 23:18
2
$\begingroup$

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.
$\endgroup$
2
  • $\begingroup$ However, this only explains what an "effect" is, and not so much about an "effect system for a language". $\endgroup$
    – Jonas
    May 23 at 22:28
  • $\begingroup$ @Jonas Good point, I've added some notes. $\endgroup$ May 24 at 9:34

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .