# Monads and Computational Types

**November 22, 2022**, tags: monad, type system.

*Monads* and *comonads* (the dual of monads) are closely related to adjunctions (Kleisli and Eilenberg-Moore), probably the most pervasive notion in Category Theory.

We intend to use monads for giving denotational semantics to programming languages, and more specifically as a way of modeling *computational types*.

in [Mog91] *Notions of Computation and Monads*:

The basic idea behind the categorical semantics below is that, in order to interpret a programming language in Category π, we distinguish the object

Aof values (of typeA) from the objectTAof computations (of typeA), and take as denotations of programs (of typeA) theelementsofTA. In particular, we identify the typeAwith the object of values (of typeA) and obtain the object of computations (of typeA) by applying an unary type-constructorTtoA. We callTanotion of computation, since it abstracts away from the type of values computations may produce.

**Example 1**. We give few notions of computation in the Category of sets.

- partiality:
*T**A*β=β*A*_{β₯}, i.e.Β*A*β +β {ββ₯β}. (β₯is the*diverging computation*) - nondeterminism:
*T**A*β=βπ«_{fin}(*A*), i.e.Β the set of finite subsets of*A*. - side-effects:
*T**A*β=β(*A*Γ*S*)^{S}, where*S*is a set of states, e.g.Β a set*U*^{L}of stores or a set of input/output sequences*U*^{*} - exceptions:
*T**A*β=β*A*β +β*E*, where*E*is the set of exceptions - continuations:
*T**A*β=β*R*^{RA}, where*R*is the set of results - interactive input:
*T**A*β=β(*ΞΌ**X***.***A*+*X*^{U}), where*U*is the set of characters. - interactive output:
*T**A*β=β(*ΞΌ**X***.***A*+(*U*Γ*X*)), i.e.Β*U*^{*}β Γβ*A*up to iso.