Effect system

Last updated February 15, 2024

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.

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:

Reading, writing or allocating memory: the effect kind is read, write, allocate or free, and the region is the point of the program where allocation was performed (i.e., each program point where allocation is performed is assigned a unique label, and region information is statically propagated along the dataflow). Most functions working with memory will actually be polymorphic in the region variable: for example, a function that swaps two locations in memory will have type forall r1 r2, unit ! {read r1, read r2, write r1, write r2}.
Working with resources, such as files: for example, the effect kind may be open, read and close, and again, the region is the point of the program where the resource is opened.
Control transfers with continuations and long jumps: the effect kind may be goto (i.e. the piece of code may perform a jump) and comefrom (i.e. the piece of code may be the target of a jump), and the region denotes the point of the program from which or to which the jump may be performed.

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

Koka is a statically typed functional programming language with algebraic effect handlers as a main feature.^[3]
Eff is a statically typed functional programming language centered around algebraic effect handlers.^[4]
Unison is a statically typed functional programming language with algebraic effect handlers (called "abilities" in the language) as a core part of the type system.^[5]
Effekt is a research language centered around effect handlers and polymorphic effects.^[6]

Full Support

Haskell is a statically typed functional programming language with several packages that allow for encoding of effects.^[7] However, Haskell is generally more focused on monads.
OCaml 5.0 introduced support for experimental effect handler primitives,^[8] with plans to introduce a proper high-level syntax in the future.

Partial Support and Prototypes

Scala 3.1 is a statically typed, functional and object oriented programming language with experimental support for effects that is limited to exceptions, in the form of a CanThrow capability.^[9]
Java is a statically typed, object oriented programming language; its checked exceptions are a relatively limited example of an effect system. Only one effect kind — throws — is available, there is no way to resume with a value, and they cannot be used with functions (only methods) unless the function implements a custom @FunctionalInterface .^[10]
JavaScript is a dynamically typed language, it has a proposal that implements algebraic effects.^[11]

Related Research Articles

In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that map values to other values, rather than a sequence of imperative statements which update the running state of the program.

ML is a functional programming language. It is known for its use of the polymorphic Hindley–Milner type system, which automatically assigns the data types of most expressions without requiring explicit type annotations, and ensures type safety; there is a formal proof that a well-typed ML program does not cause runtime type errors. ML provides pattern matching for function arguments, garbage collection, imperative programming, call-by-value and currying. While a general-purpose programming language, ML is used heavily in programming language research and is one of the few languages to be completely specified and verified using formal semantics. Its types and pattern matching make it well-suited and commonly used to operate on other formal languages, such as in compiler writing, automated theorem proving, and formal verification.

OCaml is a general-purpose, high-level, multi-paradigm programming language which extends the Caml dialect of ML with object-oriented features. OCaml was created in 1996 by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy, Ascánder Suárez, and others.

In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every term. Usually the terms are various language constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term. Type systems formalize and enforce the otherwise implicit categories the programmer uses for algebraic data types, data structures, or other components.

In computer programming, cons is a fundamental function in most dialects of the Lisp programming language. consconstructs memory objects which hold two values or pointers to two values. These objects are referred to as (cons) cells, conses, non-atomic s-expressions ("NATSes"), or (cons) pairs. In Lisp jargon, the expression "to cons x onto y" means to construct a new object with (cons xy). The resulting pair has a left half, referred to as the car, and a right half, referred to as the cdr.

In computer programming, a reference is a value that enables a program to indirectly access a particular data, such as a variable's value or a record, in the computer's memory or in some other storage device. The reference is said to refer to the datum, and accessing the datum is called dereferencing the reference. A reference is distinct from the datum itself.

In programming language theory and type theory, polymorphism is the use of a single symbol to represent multiple different types.

In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types.

<span class="mw-page-title-main">Caml</span> Programming language

Caml is a multi-paradigm, general-purpose programming language which is a dialect of the ML programming language family. Caml was developed in France at INRIA and ENS.

In computer architecture, a transport triggered architecture (TTA) is a kind of processor design in which programs directly control the internal transport buses of a processor. Computation happens as a side effect of data transports: writing data into a triggering port of a functional unit triggers the functional unit to start a computation. This is similar to what happens in a systolic array. Due to its modular structure, TTA is an ideal processor template for application-specific instruction set processors (ASIP) with customized datapath but without the inflexibility and design cost of fixed function hardware accelerators.

In computer science, a type class is a type system construct that supports ad hoc polymorphism. This is achieved by adding constraints to type variables in parametrically polymorphic types. Such a constraint typically involves a type class T and a type variable a, and means that a can only be instantiated to a type whose members support the overloaded operations associated with T.

Haxe is a high-level cross-platform programming language and compiler that can produce applications and source code for many different computing platforms from one code-base. It is free and open-source software, released under the MIT License. The compiler, written in OCaml, is released under the GNU General Public License (GPL) version 2.

In computing, ATS is a programming language designed to unify programming with formal specification. ATS has support for combining theorem proving with practical programming through the use of advanced type systems. A past version of The Computer Language Benchmarks Game has demonstrated that the performance of ATS is comparable to that of the C and C++ programming languages. By using theorem proving and strict type checking, the compiler can detect and prove that its implemented functions are not susceptible to bugs such as division by zero, memory leaks, buffer overflow, and other forms of memory corruption by verifying pointer arithmetic and reference counting before the program compiles. Additionally, by using the integrated theorem-proving system of ATS (ATS/LF), the programmer may make use of static constructs that are intertwined with the operative code to prove that a function conforms to its specification.

The expression problem is a challenging problem in programming languages that concerns the extensibility and modularity of statically typed data abstractions. The goal is to define a data abstraction that is extensible both in its representations and its behaviors, where one can add new representations and new behaviors to the data abstraction, without recompiling existing code, and while retaining static type safety. The statement of the problem exposes deficiencies in programming paradigms and programming languages, and as of 2023 is still considered unsolved, although there are many proposed solutions.

In type theory, bounded quantification refers to universal or existential quantifiers which are restricted ("bounded") to range only over the subtypes of a particular type. Bounded quantification is an interaction of parametric polymorphism with subtyping. Bounded quantification has traditionally been studied in the functional setting of System F_<:, but is available in modern object-oriented languages supporting parametric polymorphism (generics) such as Java, C# and Scala.

In computer science, region-based memory management is a type of memory management in which each allocated object is assigned to a region. A region, also called a zone, arena, area, or memory context, is a collection of allocated objects that can be efficiently reallocated or deallocated all at once. Like stack allocation, regions facilitate allocation and deallocation of memory with low overhead; but they are more flexible, allowing objects to live longer than the stack frame in which they were allocated. In typical implementations, all objects in a region are allocated in a single contiguous range of memory addresses, similarly to how stack frames are typically allocated.

Eff is a functional programming language similar in syntax to OCaml which integrates the functions of algebraic effect handlers.

Flix is a functional, imperative, and logic programming language developed at Aarhus University, with funding from the Independent Research Fund Denmark, and by a community of open source contributors. The Flix language supports algebraic data types, pattern matching, parametric polymorphism, currying, higher-order functions, extensible records, channel and process-based concurrency, and tail call elimination. Two notable features of Flix are its type and effect system and its support for first-class Datalog constraints.

Owl Scientific Computing is a software system for scientific and engineering computing developed in the Department of Computer Science and Technology, University of Cambridge. The System Research Group (SRG) in the department recognises Owl as one of the representative systems developed in SRG in the 2010s. The source code is licensed under the MIT License and can be accessed from the GitHub repository.

References

↑ Albin., Turbak, Franklyn (2010). Design concepts in programming languages. PHI Learning. ISBN 978-81-203-3996-5. OCLC 1261053520.{{cite book}}: CS1 maint: multiple names: authors list (link)
↑ Abramov, Dan. "Algebraic Effects for the Rest of Us". overreacted.io.
↑ "The Koka Manual". koka-lang.github.io.
↑ Pretnar, Matija (2021-12-07), Eff , retrieved 2021-12-11
↑ "The Unison language". www.unisonweb.org. Retrieved 2021-12-07.
↑ The Effekt research team. "Effekt Language: Concepts and Features". Effekt Language. Retrieved 2023-06-13.
↑ Vera, Josh (18 April 2020). "joshvera/freemonad-benchmark". GitHub. A benchmark comparing the performance of different free monad implementations.
↑ "OCaml - Language extensions". v2.ocaml.org. Retrieved 2023-06-13.
↑ "CanThrow Abilities". Scala Documentation. Retrieved 2021-12-07.
↑ "Java 8 Lambda function that throws exception?". Stack Overflow. Retrieved 2021-12-25.
↑ Macabeus, Bruno (16 September 2020). "macabeus/js-proposal-algebraic-effects: 📐Let there be algebraic effects in JS". GitHub.

Textbook chapters

Hankin, Chris; Nielson, Flemming; Nielson, Hanne Riis (1999). Principles of Program Analysis. Berlin: Springer. ISBN 978-3-540-65410-0.
Gifford, David; Turbak, Franklyn A.; Sheldon, Mark A. (2008). "16". Design Concepts in Programming Languages. Cambridge, Mass: MIT Press. ISBN 978-0-262-20175-9.

Overview papers

Nielson, Flemming; Nielson, Hanne Riis (1999). "Type and Effect Systems" . Correct System Design: Recent Insight and Advances. Lecture Notes in Computer Science. Springer-Verlag. 1710: 114–136. doi:10.1007/3-540-48092-7_6. ISBN 978-3-540-66624-0.