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.

strong monadarbitrary theorycall-by-push-value/Freyd multicategoryenriched category with powers and copowers
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 $V$ of “value types” and pure morphisms and a category $C$ of “comptuation types” or “linear types” and homomorphisms, where $C$ is the category of algebras of a monad on $V$. 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 $V$, but terms $\Gamma \vdash M : A$ are interpreted as Kleisli morphisms $\Gamma \to T A$, or equivalently homomorphisms of free algebras in $C$: $F \Gamma \to F A$. In call-by-name? languages, types are dually interpreted as objects of $C$, but terms $\Gamma \vdash M : A$ are interpreted as co-Kleisli morphisms $U\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.