log-book

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 A of values (of type A) from the object TA of computations (of type A), and take as denotations of programs (of type A) the elements of TA. In particular, we identify the type A with the object of values (of type A) and obtain the object of computations (of type A) by applying an unary type-constructor T to A. We call T a notion 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.

  1. partiality: TA = AβŠ₯, i.e.Β Aβ€…+β€…{ βŠ₯ }. (βŠ₯is the diverging computation)
  2. nondeterminism: TA = 𝒫fin(A), i.e.Β the set of finite subsets of A.
  3. side-effects: TA = (AΓ—S)S, where S is a set of states, e.g.Β a set UL of stores or a set of input/output sequences U*
  4. exceptions: TA = Aβ€…+β€…E, where E is the set of exceptions
  5. continuations: TA = RRA, where R is the set of results
  6. interactive input: TA = (ΞΌX.A+XU), where U is the set of characters.
  7. interactive output: TA = (ΞΌX.A+(UΓ—X)), i.e.Β U*β€…Γ—β€…A up to iso.