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. The design of a categorical semantics for non-functional computational
languages
is still an open
question, relying on fundamental results based on monads.
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 is hidden
in the syntax. 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 function f:A->B stands
for a function f':A->TB, which requires the existence of some
process for safely composing f':A->TB and g':B->TC as
(g.f)':A->TC : in categorical terms, this property is ensured when T
is a monad [Moggi
1991, Haskell]. For instance, the
monad
for states is TX=(SxX)^S where S is made of the states, and the monad
for
exceptions is TX=X+E where E is made of the exceptions. In order to
deal with the operations and equations associated to each effect, this
approach has been translated in terms of Lawvere
theories [Plotkin-Power 2002]. For instance, the Lawvere
theory for states is the free countable Lawvere theory generated by the
operations lookup and update subject to seven equations, and the
Lawvere theory for exceptions is the free Lawvere theory generated by E
operations raise:0->1.
Our definition of effects relies on the fact that an effect is defined
from a span of logics: an "apparent" logic is associated to the syntax,
an "explicit" logic to the semantics, and they are related by a
"decorated" logic which is suitable both for the syntax and for the
semantics, but which is an "unusual" kind logic. The relevant notions
of logic and morphisms between them are provided by the theory of diagrammatic logics.
Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse,
Jean-Claude
Reynaud. States and exceptions considered as dual effects.
[hal-00445873] arXiv:1001.1662
(new version, 2011) Submitted for publication.
Jean-Guillaume Dumas, Dominique Duval, Jean-Claude Reynaud.
Cartesian effect categories are Freyd-categories. Journal of Symbolic
Computation 46 p. 272-293 (2011) [hal-00369328] arXiv:0903.3311.
[Duval 2007] Dominique Duval. Diagrammatic inference. http://arxiv.org/abs/0710.1208 (2007).
[Duval-Reynaud
2005]
D. Duval, J.-C. Reynaud.
Diagrammatic
logic
and
exceptions:an
introduction.
Mathematics, Algorithms, Proofs, T.
Coquand, H. Lombardi, M. Roy (Eds.), Dagstuhl
Seminar 05021,
09.01. - 14.01.2005
[Duval 2003]
D. Duval. Diagrammatic
Specifications. Reproduced from Mathematical Structures in Computer
Science (13)
857-890 (2003), with permission from Cambridge
University
Press.
[Duval-Lair 2002] Version
préliminaire
:
D.
Duval, C. Lair. Diagrammatic
Specifications.
Rapport de Recherche IMAG-LMC 1043 M (2002)