Algebras for Algebraic Effects: Behavioural Equivalence of Effectful Programs
Tallinn University of Technology
Abstract:
Algebraic effects describe interactions between a program and its
environment, for instance to resolve some probabilistic choice, or to
communicate with some global store. Algebraic effects in particular
can be described using algebraic effect operations in the programming
language. To give behavioural descriptions of effects we use algebras
over a monad, which e.g. calculate expectations for probabilistic
languages, or find the weakest precondition for programs interacting
with a global store. If such algebras are sufficiently nice, they can
be used to formulate a congruent notion of program equivalence.
We will look at different algebras for describing functional languages
including algebraic effects such as nondeterminism, probability,
global store, timer, and combinations thereof. We will moreover look
at two methods for using these algebras to specify a notion of program
equivalence: one by using them as quantitative modalities in a
quantitative logic of behavioural properties, and one by constructing
a relator used to define applicative bisimilarity. Lastly, we will
briefly discuss more recent work: deriving algebras from equational
theories, and combining effects and their algebras.