Monads as a Solution for Generalized Opacity

In this paper we discuss a conservative ex-tension of the simply-typed lambda calcu-lus in order to model a class of expres-sions that generalize the notion of opaque contexts. Our extension is based on previ-ous work in the semantics of programming languages aimed at providing a mathemat-ical characterization of computations that produce some kind of side effect (Moggi, 1989), and is based on the notion of mon-ads, a construction in category theory that, intuitively, maps a collection of “simple” values and “simple ” functions into a more complex value space, in a canonical way. The main advantages of our approach with respect to traditional analyses of opacity are the fact that we are able to explain in a uniform way a set of different but re-lated phenomena, and that we do so in a principled way that has been shown to also explain other linguistic phenomena (Shan, 2001).