What is a type and effect system?

Question

The Wikipedia article on Effect system is currently just a short stub and I've been wondering for a while as to what is an effect system.

• Are there any languages that have an effect system in addition to a type system?
• What would a possible (hypothetical) notation in a mainstream language, that you're familiar, with look like with effects?

Answer 1

A "type and effect system" describes not only the kinds of values in a program, but the changes in those values. "Typestate" checking is a related idea.

An example might be a type system that tracks file handles: instead of having a function close with return type void, the type system would record the effect of close as disposing of the file resource—any attempt to read from or write to the file after calling close would become a type error.

I'm not aware of any type and effect system appearing in a mainstream programming language. They have been used to define static analyses (for example, it's quite natural to define an analysis for proper locking/unlocking in terms of effects). As such, effect systems are usually defined using inference schemes rather than concrete syntax. You could imagine a syntax looking something like

File open(String name) [+File]; // open creates a new file handle
void close(File f)     [-f]   ; // close destroys f 

If you want to learn more, the following papers might be interesting (fair warning: the papers are quite theoretical).

• Types for Atomicity: Static Checking and Inference for Java. Flanagan, Freund, Lipshin, and Qadeer.
• Enforcing High-Level Protocols in Low-Level Software. Robert DeLine and Manuel Fändrich.
• Type and Effect Systems. Nielson and Nielson.

Answer 2

(This is not an authoritative answer; just trying to trawl my memory.)

In a sense, any time you code a 'state monad' in a language, you're using the type system as a potential effect system. So "State" or "IO" in Haskell capture this notion (IO captures a whole lot of other effects as well). I vaguely remember reading papers about various languages that use advanced type systems including things like "dependent types" to control finer-grained management of effects, so that for instance the type/effect system could capture information about which memory locations would be modified in a given data type. This is useful, as it provides ways to make two functions that modify mutually exclusive bits of state be allowed to "commute" (monads don't typically commute, and different monads don't always compose well with one another, which often makes it hard to type (read: assign a static type to) 'reasonable' programs)...

An analogy at a very hand-wavy level is how Java has checked exceptions. You express extra information in the type system about certain effects (you can think of an exception as an 'effect' for the purpose of the analogy), but these 'effects' typically leak out all over your program and don't compose well in practice (you end up with a million 'throws' clauses or else resort to lots of unchecked runtime exception types).

I think a lot of research is being done in this area, both for research-y and mainstream-y languages, as the ability to annotate functions with effect information can unlock the compiler's ability to do a number of optimizations, can impact concurrency, and can do great things for various program analyses and tooling. I don't personally have high hopes for it any time soon, though, as I think lots of smart people have been working on it for a long time and there's still very little to show for it.