ABSTRACT
In functional programming, monadic characterizations of computational effects are normally understood denotationally: they describe how an effectful program can be systematically expanded or translated into a larger, pure program, which can then be evaluated according to an effect-free semantics. Any effect-specific operations expressible in the monad are also given purely functional definitions, but these definitions are only directly executable in the context of an already translated program. This approach thus takes an inherently Church-style view of effects: the nominal meaning of every effectful term in the program depends crucially on its type.
We present here a complementary, operational view of monadic effects, in which an effect definition directly induces an imperative behavior of the new operations expressible in the monad. This behavior is formalized as additional operational rules for only the new constructs; it does not require any structural changes to the evaluation judgment. Specifically, we give a small-step operational semantics of a prototypical functional language supporting programmer-definable, layered effects, and show how this semantics naturally supports reasoning by familiar syntactic techniques, such as showing soundness of a Curry-style effect-type system by the progress+preservation method.
- Robert Cartwright and Matthias Felleisen. Extensible denotational language specifications. In Masami Hagiya and John C. Mitchell, editors, Symposium on Theoretical Aspects of Computer Software, volume 789 of Lecture Notes in Computer Science, pages 244--272, Sendai, Japan, April 1994. Google ScholarDigital Library
- Karl Crary and Robert Harper. Syntactic logical relations for polymorphic and recursive types. Electronic Notes in Theoretical Computer Science, 172, 2007. Google ScholarDigital Library
- Matthias Felleisen and Robert Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103(2):235--271, September 1992. Google ScholarDigital Library
- Andrzej Filinski. Representing layered monads. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 175--188, San Antonio, Texas, January 1999. Google ScholarDigital Library
- Andrzej Filinski. On the relations between monadic semantics. Theoretical Computer Science, 375(1-3):41--75, 2007. Google ScholarDigital Library
- Andrzej Filinski and Kristian Støvring. Inductive reasoning about effectful data types. In ICFP'07: Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming, pages 97--110. ACM Press, October 2007. Google ScholarDigital Library
- Marcelo Fiore and Gordon D. Plotkin. An axiomatisation of computationally adequate domain theoretic models of FPC. In Proceedings of the Ninth Symposium on Logic in Computer Science, pages 92--102, Paris, France, 1994.Google ScholarCross Ref
- Carl A. Gunter, Didier Remy, and Jon G. Riecke. A generalization of exceptions and control in ML-like languages. In Functional Programming and Computer Architecture, pages 12--23, 1995. Google ScholarDigital Library
- Oleg Kiselyov, Chung chieh Shan, and Amr Sabry. Delimited dynamic binding. In ICFP'06: Proceedings of the 11th International Conference on Functional Programming, pages 26--37, 2006. Google ScholarDigital Library
- Paul Blain Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation, 19(4):377--414, 2006. Google ScholarDigital Library
- Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, 1971.Google Scholar
- Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pages 14--23, Pacific Grove, California, June 1989. IEEE. Google ScholarCross Ref
- Luc Moreau. A syntactic theory of dynamic binding. Higher-Order and Symbolic Computation, 11(3):233--279, 1998. Google ScholarDigital Library
- Peter D. Mosses. Modular structural operational semantics. Journal of Logic and Algebraic Programming, 60-61:195--228, 2004.Google ScholarCross Ref
- Frank Pfenning. Substructural operational semantics and linear destination-passing style (abstract). In Proceedings of the 2nd Asian Symposium on Programming Languages and Systems (APLAS'04), volume 3302 of Lecture Notes in Computer Science, page 196, 2004.Google ScholarCross Ref
- Frank Pfenning and Carsten Schurmann. System description: Twelf - a meta-logical framework for deductive systems. In 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Computer Science, pages 202--206, 1999. Google ScholarDigital Library
- Benjamin Pierce. Types and Programming Languages. MIT Press, 2002. Google ScholarDigital Library
- Gordon D. Plotkin and John Power. Algebraic operations and generic effects. Applied Categorical Structures, 11(1):69--94, 2003.Google ScholarCross Ref
- Gordon D. Plotkin and Matija Pretnar. Handlers of algebraic effects. In 18th European Symposium on Programming, volume 5502 of Lecture Notes in Computer Science, pages 80--94, March 2009. Google ScholarDigital Library
- Philip Wadler. Comprehending monads. In Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 61--78, Nice, France, June 1990. Google ScholarDigital Library
- Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, 1994. Google ScholarDigital Library
Index Terms
- Monads in action
Recommendations
On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control
We compare the expressive power of three programming abstractions for user-defined computational effects: Plotkin and Pretnar's effect handlers, Filinski's monadic reflection, and delimited control without answer-type-modification. This comparison ...
Monads in action
POPL '10In functional programming, monadic characterizations of computational effects are normally understood denotationally: they describe how an effectful program can be systematically expanded or translated into a larger, pure program, which can then be ...
Coproducts of Monads on Set
LICS '12: Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer ScienceCoproducts of monads on $\Set$ have arisen in both the study of computational effects and universal algebra. We describe coproducts of consistent monads on $\Set$ by an initial algebra formula, and prove also the converse: if the coproduct exists, so do ...
Comments