The marriage of effects and monads

ABSTRACT

Gifford and others proposed an effect typing discipline to delimit the scope of computational effects within a program, while Moggi and others proposed monads for much the same purpose. Here we marry effects to monads, uniting two previously separate lines of research. In particular, we show that the type, region, and effect system of Talpin and Jouvelot carries over directly to an analogous system for monads, including a type and effect reconstruction algorithm. The same technique should allow one to transpose any effect system into a corresponding monad system.

REFERENCES

• 1: Barthe, G., Hatcliff, J., and Thiemann, P. 1998. Monadic type systems: Pure type systems for impure settings (preliminary report). In Proceedings of HOOTS'97. Electronic Notes in Theoretical Computer Science, vol. 10. Elsevier, Amsterdam, The Netherlands.
• 2: Nick Benton , Andrew Kennedy , George Russell, Compiling standard ML to Java bytecodes, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.129-140, September 26-29, 1998, Baltimore, Maryland, United States
• 3: Val Breazu-Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov, Inheritance as implicit coercion, Information and Computation, v.93 n.1, p.172-221, July 1991 [doi>10.1016/0890-5401(91)90055-7]
• 4: Sigbjorn Finne , Daan Leijen , Erik Meijer , Simon Peyton Jones, Calling hell from heaven and heaven from hell, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.114-125, September 27-29, 1999, Paris, France
• 5: Gifford, D. K., Jouvelot, P., Lucassen, J. M., and Sheldon, M. A. 1987. FX-87 Reference Manual. Tech. Rep. MIT/LCS/TR-407, MIT Laboratory for Computer Science, Cambridge, MA.
• 6: David K. Gifford , John M. Lucassen, Integrating functional and imperative programming, Proceedings of the 1986 ACM conference on LISP and functional programming, p.28-38, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319848]
• 7: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 8: Robert Harper , Mark Lillibridge, Polymorphic type assignment and CPS conversion, Lisp and Symbolic Computation, v.6 n.3-4, p.361-380, Nov. 1993 [doi>10.1007/BF01019463]
• 9: John Hatcliff , Olivier Danvy, A generic account of continuation-passing styles, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.458-471, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.178053]
• 10: Jouvelot, P. and Gifford, D. K. 1989. Reasoning about continuations with control effects. Tech. Rep. MIT/LCS/TM-378, MIT Laboratory for Computer Science, Cambridge, MA.
• 11: John Launchbury , Simon L. Peyton Jones, Lazy functional state threads, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.24-35, June 20-24, 1994, Orlando, Florida, United States
• 12: Xavier Leroy, Polymorphism by name for references and continuations, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.220-231, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158632]
• 13: Lucassen, J. M. 1987. Types and effects, towards the integration of functional and imperative programming. Tech. Rep. MIT/LCS/TR-408, MIT Laboratory for Computer Science, Cambridge, MA. (Also a Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, MA, 1987.)
• 14: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 15: Milner, R. 1978. A theory for type polymorphism in programming. J. Comput. Syst. Sci. 17, 348--375.
• 16: Robin Milner , Mads Tofte , Robert Harper, The Definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 17: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 18: Mitchell, J. C. 1991. Type inference with simple subtypes, J. Funct. Programm. 1, 3, 245--286.
• 19: E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
• 20: Eugenio Moggi, Notions of computation and monads, Information and Computation, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
• 21: Moggi, E. and Palumbo, F. 1999. Monadic encapsulation of effects: A revised approach. HOOTS '99: Higher Order Operational Techniques in Semantics. Electronic Notes in Theoretical Computer Science, vol. 26. Elsevier, Amsterdam, The Netherlands.
• 22: Hanne Riis Nielson , Flemming Nielson , Torben Amtoft, Polymorphic Subtyping for Effect Analysis: The Static Semantics, Selected papers from the 5th LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages, p.141-171, June 24-26, 1996
• 23: Simon Peyton Jones , Andrew Gordon , Sigbjorn Finne, Concurrent Haskell, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.295-308, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237794]
• 24: Peyton Jones, S. and Hughes, J., Eds. 1999. Haskell98, a non-strict, purely functional language. Available at http://www.haskell.org, December 1998.
• 25: Simon Peyton Jones , Alastair Reid , Fergus Henderson , Tony Hoare , Simon Marlow, A semantics for imprecise exceptions, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.25-36, May 01-04, 1999, Atlanta, Georgia, United States
• 26: Simon L. Peyton Jones , Philip Wadler, Imperative functional programming, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.71-84, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158524]
• 27: Plotkin, G. 1975. Call-by-name, call-by-value, and the λ-calculus. Theoret. Comput. Sci. 1, 125--159.
• 28: Amr Sabry , Philip Wadler, A reflection on call-by-value, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.6, p.916-941, Nov. 1997 [doi>10.1145/267959.269968]
• 29: Miley Semmelroth , Amr Sabry, Monadic encapsulation in ML, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.8-17, September 27-29, 1999, Paris, France
• 30: Talpin, J.-P. 1993. Theoretical and practical aspects of type and effect inference. Ph.D. thesis, Ecole des Mines de Paris and University Paris VI, Paris, France.
• 31: Talpin, J.-P. and Jouvelot, P. 1992. Polymorphic type, region, and effect inference. J. Funct. Programm.2, 3 (July), 245--271.
• 32: Jean-Pierre Talpin , Pierre Jouvelot, The type and effect discipline, Information and Computation, v.111 n.2, p.245-296, June 1994 [doi>10.1006/inco.1994.1046]
• 33: Tofte, M. 1987. Operational semantics and polymorphic type inference. Ph.D. thesis, University of Edinburgh, Edinburgh, Scotland.
• 34: Mads Tofte , Lars Birkedal, A region inference algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.4, p.724-767, July 1998 [doi>10.1145/291891.291894]
• 35: Mads Tofte , Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.188-201, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177855]
• 36: Andrew P. Tolmach, Optimizing ML Using a Hierarchy of Monadic Types, Proceedings of the Second International Workshop on Types in Compilation, p.97-115, March 25-27, 1998
• 37: Philip Wadler, Comprehending monads, Proceedings of the 1990 ACM conference on LISP and functional programming, p.61-78, June 27-29, 1990, Nice, France [doi>10.1145/91556.91592]
• 38: Philip Wadler, The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143169]
• 39: Philip Wadler, Monads for Functional Programming, Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text, p.24-52, May 24-30, 1995
• 40: Wadler, P. 1995. How to declare an imperative (Invited talk). International Logic Programming Symposium (Portland, OR). MIT Press, Cambridge, MA.
• 41: Philip Wadler, The marriage of effects and monads, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.63-74, September 26-29, 1998, Baltimore, Maryland, United States
• 42: Andrew K. Wright, Typing references by effect inference, Symposium proceedings on 4th European symposium on programming, p.473-491, January 1992, Rennes, France
• 43: Andrew K. Wright, Simple imperative polymorphism, Lisp and Symbolic Computation, v.8 n.4, p.343-355, Dec. 1995 [doi>10.1007/BF01018828]
• 44: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

General Terms:
Languages, Theory

Keywords:
Monad, effect, region, type, type reconstruction