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 systems into a corresponding monad system.

REFERENCES

• BKR98: 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
• BCGS91: Val Breazu-Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov, Inheritance as implicit coercion, Theoretical aspects of object-oriented programming: types, semantics, and language design, MIT Press, Cambridge, MA, 1994
• GL86: 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]
• GJLS87: D.K. Gifford, P. Jouvelot, J. M. Lucassen, and M. A. Sheldon, FX-87 Reference Manual, Technical report MIT/LCS/TR-407, MiT Laboratory for Computer Science, September 1987.
• GJS96: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• HD94: 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]
• JG89: P. Jouvelot and D. K. Gifford, Reasoning about continuations with control effects, Technical report MIT/LCS/TM-378, MIT Laboratory for Computer Science, January 1989.
• Jon95: Mark P. Jones, Functional Programming with Overloading and Higher-Order Polymorphism, Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text, p.97-136, May 24-30, 1995
• LP94: 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
• Luc87: J. M. Lucassen, Types and effects, towards the integration of functional and imperative programming, Ph.D. Thesis, Technical report MIT/LCS/TR-408, MIT Laboratory for Computer Science, August 1987.
• Mil78: R. Milner, A theory for type polymorphism in prog-ramming, Journal of Computer and Systems Science, 17:348-375, 1978.
• Mit91: J. C. Mitchell, Type inference with simple subtypes, Journal of Functional Programming, 1(3):245- 286, 1991.
• Mit96: John C. Mitchell, Foundations of programming languages, MIT Press, Cambridge, MA, 1996
• MTH90: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• MTHM97: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• Mog89: 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
• Mog91: 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]
• PH97: J. Peterson and K. Hammond, editors, Haskell 1.4, a non-strict, purely functional language, Technical report, Yale University, April 1997.
• Plo75: G. Plotkin, Call-by-name, call-by-value, and the A-calculus, Theoretical Computer Science, 1:125-159, 1975.
• PW93: 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]
• SW97: 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]
• TJ92: J.-P. Talpin and P. Jouvelot, Polymorphic type, region, and effect inference, Journal of Functional Programming, 2(3):245-271, July 1992.
• TJ94: 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]
• Tof87: M. Torte, Operational semantics and polymorphic type inference, PhD Thesis, University of Edinburgh, 1987.
• TB98: 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]
• Tol98: 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
• Wad90: 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]
• Wad92: 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]
• Wad93: 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
• Wad95: P. Wadler, How to declare an imperative (Invited talk), International Logic Programming Symposium, Portland, Oregon, MiT Press, December 1995.
• WF94: 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]
• Wri92: Andrew K. Wright, Typing references by effect inference, Symposium proceedings on 4th European symposium on programming, p.473-491, January 1992, Rennes, France
• Wri95: Andrew K. Wright, Simple imperative polymorphism, Lisp and Symbolic Computation, v.8 n.4, p.343-355, Dec. 1995 [doi>10.1007/BF01018828]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

General Terms:
Algorithms, Design, Languages, Performance, Theory