Adequacy for Algebraic Effects
View/ Open
Date
2002Author
Plotkin, Gordon
Power, John
Metadata
Abstract
Moggi proposed a monadic account of computational effects.
He also presented the computational lamda-calculus, c, a core call-by-value
functional programming language for effects; the effects are obtained by
adding appropriate operations. The question arises as to whether one
can give a corresponding treatment of operational semantics. We do
this in the case of algebraic e ects where the operations are given by
a single-sorted algebraic signature, and their semantics is supported by
the monad, in a certain sense. We consider call-by-value PCF with—
and without—recursion, an extension of c with arithmetic. We prove
general adequacy theorems, and illustrate these with two examples: non-
determinism and probabilistic nondeterminism.