Side effect monad, its equational theory and applications

Olha Sharavska

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