## Side effect monad, its equational theory and applications

Institute of Cybernetics

Thursday, 15 Dec. 2005, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

**Abstract**: A pure functional program leaves input data intact
due to absence of side effects -- variable and field updates. This
eases formal reasoning about computations, but makes programming less
flexible and leads to inefficient usage of memory.

E. Moggi proposed monads to formalise functional computations with
non-functional features. It is known that to give a monad is the same
as to give an equational theory for effects that generate the monad.
G. Plotkin and J. Power researched the theory of "select" and "update"
operations on memory, which determine the side-effect monad.

We will discuss the possibility to apply these results for
operating databases. The group of B. Pierce has developed a concept of
"lenses" which perform exchange of information between abstract and
concrete bases. We show, that a lens, satisfying 3 equational axioms,
defines a map of monads.

Tarmo Uustalu

Last update 18.12.2005