Abstract
Given a complete and cocomplete symmetric monoidal closed category V and a symmetric monoidal V-category C with cotensors and a strong V-monad T on C, we investigate axioms under which an Ob C-indexed family of operations of the form α x :(Tx)v→(Tx)w provides semantics for algebraic operations on the computational λ-calculus. We recall a definition for which we have elsewhere given adequacy results, and we show that an enrichment of it is equivalent to a range of other possible natural definitions of algebraic operation. In particular, we define the notion of generic effect and show that to give a generic effect is equivalent to giving an algebraic operation. We further show how the usual monadic semantics of the computational λ-calculus extends uniformly to incorporate generic effects. We outline examples and non-examples and we show that our definition also enriches one for call-by-name languages with effects.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Anderson, S. O. and Power, A. J.: A Representable approach to finite nondeterminism, Theoretical Computer Science 177(1) (1997), 3–25.
Benton, N., Hughes, J. and Moggi, E.: Monads and effects, in Advanced Lectures from International Summer School on Applied Semantics (eds. Barthe, G., Dybjer, P., Pinto, L. and Saraiva, J.), Lecture Notes in Computer Science, Vol. 2395, pp. 42–122, Springer-Verlag, Berlin, 2002.
Day, B.: On closed categories of functors, in Reports of the Midwest Category Seminar IV, Lecture Notes in Math. 137, Springer-Verlag, Berlin, 1970, pp. 1–38.
Dubuc, E.: Kan Extensions in Enriched Category Theory, Lecture Notes in Math. 145, Springer-Verlag, Berlin, 1970.
Fuhrmann, C. and Thielecke, H.: On the call-by-value CPS transform and its semantics, Information and Computation, to appear.
Heckmann, R.: Probabilistic domains, in Proc. CAAP '94, Lecture Notes in Computer Science 136, Springer-Verlag, Berlin, 1994, pp. 21–56.
Hyland, M., Plotkin, G. D. and Power, A. J.: Combining computational effects: Commutativity and sum, in R. Baeza-Yates, U. Montanari and N. Santoro (eds), Foundations of Information Technology in the Era of Network and Mobile Computing, pp. 474–484, Kluwer, 2002.
Jones, C.: Probabilistic non-determinism, Ph.D. Thesis, University of Edinburgh, Report ECSLFCS-90-105, 1990.
Jones, C. and Plotkin, G. D.: A probabilistic powerdomain of evaluations, in Proceedings of the 4th LICS, Asilomar, IEEE Press, Washington, 1989, pp. 186–195.
Kelly, G. M.: Basic Concepts of Enriched Category Theory, Cambridge University Press, Cambridge, 1982.
Levy, P. B.: Call-by-push-value: A subsuming paradigm, in J.-Y. Girard (ed.), Proc. TLCA '99, Lecture Notes in Computer Science 1581, Springer-Verlag, Berlin, 1999, pp. 228–242.
Mac Lane, S.: Categories for the Working Mathematician, Springer-Verlag, Berlin, 1971.
Moggi, E.: Computational lambda-calculus and monads, in Proceedings of LICS '89, IEEE Press, Washington, 1989, pp. 14–23.
Moggi, E.: An abstract view of programming languages, University of Edinburgh, Report ECSLFCS-90-113, 1989.
Moggi, E.: Notions of computation and monads, Information and Computation 93(1) (1991), 55–92.
O'Hearn, P. W. and Tennent, R. D.: Algol-like Languages, Progress in Theoretical Computer Science, Birkhäuser, Boston, 1997.
Milner, R., Tofte, M., Harper, R. and MacQueen, D.: The Definition of Standard ML – Revised, MIT Press, Cambridge, 1997.
Plotkin, G. D.: A powerdomain construction, SIAM Journal on Computing 5(3) (1976), 452–487.
Plotkin, G. D.: Domains, http://www.dcs.ed.ac.uk/home/gdp/, 1983.
Plotkin, G. D. and Power, A. J.: Adequacy for algebraic effects, in F. Honsell and M. Miculan (eds), Proceedings of FOSSACS '01, Lecture Notes in Computer Science 2030, Springer-Verlag, Berlin, 2001, pp. 1–24.
Plotkin, G. D. and Power, A. J.: Semantics for algebraic operations (extended abstract), in S. Brookes and M. Mislove (eds), Proceedings of MFPS XVII, Electronic Notes in Theoretical Computer Science 45, Elsevier, Amsterdam, 2001.
Plotkin, G. D. and Power, A. J.: Notions of computation determine monads, in M. Nielsen and U. Engberg (eds), Proceedings of FOSSACS '02, Lecture Notes in Computer Science 2303, Springer-Verlag, Berlin, 2002, pp. 342–356.
Power, A. J.: Enriched Lawvere theories, in Theory and Applications of Categories, 2000, pp. 83–93.
Power, A. J.: Models for the computational lambda calculus, in T. Hurley, M. Mac an Airchinnigh, M. Schellekens and A. K. Seda (eds), Proceedings of MFCSIT 2000, Electronic Notes in Theoretical Computer Science 40, Elsevier, Amsterdam, 2001.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Plotkin, G., Power, J. Algebraic Operations and Generic Effects. Applied Categorical Structures 11, 69–94 (2003). https://doi.org/10.1023/A:1023064908962
Issue Date:
DOI: https://doi.org/10.1023/A:1023064908962