Back to Beck: the state monad and the continuation monad from the viewpoint of monadicity

Feng, Yuning (2024). Back to Beck: the state monad and the continuation monad from the viewpoint of monadicity. University of Birmingham. Ph.D.

Preview

Feng2024PhD.pdf
Text - Accepted Version
Available under License All rights reserved.
Download (1MB) | Preview

Abstract

We introduce control algebras, which are algebras of two operations called call/cc and abort. The two operations are natural ones among programs that manipulate their plan of work. The significance of the formulation is that it is operationally natural, yet the notion of algebras is equivalent to the established notion of monad algebras, where the monad is the continuation monad.

We also consider the control effect and the state effect from the perspective of Beck's monadicity theorem. In particular, we notice connections between operationally meaningful objects in the two effects and coequalisers of Beck's pair; the latter are important ingredients in Beck's monadicity theorem. In the case of control, Beck's coequaliser is the set of continuations of the algebra in concern; in the case of state, that coequaliser is the set of determined elements, i.e., elements in the algebra where preceding with update operations would have no effect.

Type of Work:

Thesis (Doctorates > Ph.D.)

Award Type:

Doctorates > Ph.D.

Supervisor(s):