nLab side effect

Contents

Contents

Idea

In computer science, a side effect refers simply to the modification of some kind of state, such as changing the value of a variable, writing some data to disk or raising an exception.

Relation to Monads and Algebras and Multicategories

The presence of side effects in a programming language usually means the language cannot be given a denotational semantics in the category of sets, or in any bicartesian closed category. Instead, they can be interpreted in the category of algebras of a monad on a bicartesian closed category, often a monad presented by an algebraic theory. There is a direct relationship between properties of the monad or theory and the type theoretic syntax that can be interpreted in its category of algebras.

monadsalgebraic theoriesflavor of multicategorytypical model
strong monadarbitrary theorycall-by-push-value/Freyd multicategoryenriched category with powers and copowers
monoidal monadcommutative algebraic theorylinear logic/linear-non-linear logicsymmetric monoidal closed category/linear-non-linear adjunction
affine monadaffine algebraic theory?affine logicsemicartesian monoidal category
relevant monad?relevant algebraic theory?relevance logicrelevance monoidal category
preserves cartesian productsaffine and relevant theorycartesian multicategory/S4monoidal adjunction between bicartesian closed? categories

So in typical models, you have a category VV of “value types” and pure morphisms and a category CC of “comptuation types” or “linear types” and homomorphisms, where CC is the category of algebras of a monad on VV. Then, how the types and terms of a language are interpreted in the model depends on the evaluation order? of the language. In call-by-value? languages, types are interpreted as objects of VV, but terms ΓM:A\Gamma \vdash M : A are interpreted as Kleisli morphisms ΓTA\Gamma \to T A, or equivalently homomorphisms of free algebras in CC: FΓFAF \Gamma \to F A. In call-by-name? languages, types are dually interpreted as objects of CC, but terms ΓM:A\Gamma \vdash M : A are interpreted as co-Kleisli morphisms UΓUAU\Gamma \to U A.

A dual approach would be to start with a category of linear morphisms and construct a category of “value types” as the category of coalgebras of some well-behaved comonad. This approach is advocated by Girard in his original work on linear logic.

References

The conditions on monads above and their relationship to structural rules are described in the following (though the notions themselves are originally due to Anders Kock).

On side effects in dependent (linear) type theory:

Last revised on August 21, 2022 at 04:16:35. See the history of this page for a list of all contributions to it.