Adequacy for Algebraic Effects

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.