** 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
of`x` 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.