Dominique Duval

Semantics of computational effects


It is well-known that simply-typed lambda calculus can be interpreted in any cartesian closed category. However, many computational languages are not functional, they have various kinds of effects (input and output, non-termination, states, exceptions,...). The design of a categorical semantics for non-functional computational languages is still a challenging issue.

An effect in a computational language can be defined as an "apparent lack of soundness": something which is necessary for understanding the semantics of the programs cannot be seen easily in its syntax. So that there is an apparent mismatch between the syntax and the denotational semantics of the language. For instance, the state of the memory never appears explicitly in an imperative program, although most parts of the program are written in view of modifying it. In a similar way, in object-oriented programming the state of an object does not appear explicitly as a parameter or as a result of the methods, although most methods use or modify this state.

Typically, there is an effect when a syntactic term f:A->B is not interpreted as a function f:A->B but as "something else". Quite often, this "something else" is simply a function f':HA->HB for some functor H; this includes the case where H is a monad T and f' is defined from some f'':A->TB and the case where H is a comonad D and f' is defined from some f'':DA->B. For instance, the functor H for states is the product comonad HX=S*X where S is the set of states, while the functor H for exceptions is the coproduct monad HX=X+E where E is the set of exceptions. Then, the combination of effects is essentially the composition of the corresponding functors.

Instead of introducing explicitly the functor H, we derive equational rules "with decorations" for proving properties of progams with computational effects.

As a toy example, let us consider a class BankAccount for managing (very simple!) bank accounts. In the class BankAccount, there is a method int balance() const which returns the current balance of the account and a method void deposit(int x) for the deposit ofx Euros on the account. The deposit method is a modifier ("read-write"), which means that it can use and modify the state of the current account. The balance method is an accessor ("read-only"), which means that it can use the state of the current account but it is not allowed to modify this state, this is specified by the keyword const. Syntactically, methods look like functions: here, deposit:int->void and balance:void->int. But these methods are interpreted as the functions deposit':state*int->state and balance'':state->int, where state is the set of states. In our approach, "decorations" are used for classifying the operations and methods according to their interaction with the state: the decorations (1) and (2) correspond respectively to the object-oriented notions of accessor and modifier, so that deposit^(1):int->void and balance^(2):void->int. In addition, the decoration (0) is assigned to pure expressions, which neither use nor modify the state. The usual rules of equational logic are also "decorated", so as to take into account the interaction of the methods with the hidden state.

See my Publications with César Domínguez, Jean-Guillaume Dumas, Burak Ekici, Laurent Fousse, Damien Pous and Jean-Claude Reynaud and their bibliography.