Skip to main content
SpringerLink
Log in
Book cover

International Summer School on Applied Semantics

APPSEM 2000: Applied Semantics pp 42–122Cite as

Monads and Effects

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2395))

Abstract

A tension in language design has been between simple semantics on the one hand, and rich possibilities for side-effects, exception handling and so on on the other. The introduction of monads has made a large step towards reconciling these alternatives. First proposed by Moggi as a way of structuring semantic descriptions, they were adopted by Wadler to structure Haskell programs. Monads have been used to solve long-standing problems such as adding pointers and assignment, inter-language working, and exception handling to Haskell, without compromising its purely functional semantics. The course introduces monads, effects, and exemplifies their applications in programming (Haskell) and in compilation (MLj). The course presents typed metalanguages for monads and related categorical notions, and then describes how they can be further refined by introducing effects.

Research partially supported by MURST and ESPRIT WG APPSEM.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. W. Appel. Compiling with Continuations. Cambridge University Press, 1992.

    Google Scholar 

  2. P. N. Benton, G. M. Bierman, and V. C. V. de Paiva. Computational types from a logical perspective. Journal of Functional Programming, 8(2):177–193, March 1998. Preliminary version appeared as Technical Report 365, University of Cambridge Computer Laboratory, May 1995.

    Google Scholar 

  3. P. N. Benton. Strictness Analysis of Lazy Functional Programs. PhD thesis, Computer Laboratory, University of Cambridge, December 1992.

    Google Scholar 

  4. A. Banerjee, N. Heintze, and J. G. Reicke. Region analysis and the polymorphic lambda calculus. In Fourteenth IEEE Symposium on Logic and Computer Science, 1999.

    Google Scholar 

  5. G. Barthe, J. Hatcliff, and P. Thiemann. Monadic type systems: Pure type systems for impure settings. In Proceedings of the Second HOOTS Workshop, Stanford University, Palo Alto, CA. December, 1997, Electronic Notes in Theoretical Computer Science. Elsevier, February 1998.

    Google Scholar 

  6. N. Benton and A. Kennedy. Monads, effects and transformations. In Third International Workshop on Higher Order Operational Techniques in Semantics (HOOTS), Paris, volume 26 of Electronic Notes in Theoretical Computer Science. Elsevier, September 1999.

    Google Scholar 

  7. N. Benton and A. Kennedy. Exceptional syntax. Journal of Functional Programming, 11(4):395–410, July 2001.

    Google Scholar 

  8. N. Benton, A. Kennedy, and G. Russell. Compiling Standard ML to Java bytecodes. In 3rd ACM SIGPLAN Conference on Functional Programming, September 1998.

    Google Scholar 

  9. G. L. Burn and D. Le Metayer. Proving the correctness of compiler optimisations based on a global program analysis. Technical Report Doc 92/20, Department of Computing, Imperial College, London, 1992.

    Google Scholar 

  10. P. Buneman, S. Naqvi, V. Tannen, and L. Wong. Principles of programming with complex objects and collection types. Theoretical Computer Science, 149(1), 1995.

    Google Scholar 

  11. F. Borceux. Handbook of Categorial Algebra. Cambridge University Press, 1994.

    Google Scholar 

  12. Erik Barendsen and Sjaak Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, pages 579–612, 1996.

    Google Scholar 

  13. W. Burge. Recursive Programming Techniques. Addison-Wesley Publishing Company, Reading, Mass., 1975.

    MATH  Google Scholar 

  14. M. Barr and C. Wells. Toposes, Triples and Theories. Springer, 1985.

    Google Scholar 

  15. R. Cartwright and M. Felleisen. Extensible denotational language specifications. In Theoretical Aspects of Computer Software, volume 789 of LNCS. Springer, 1994.

    Google Scholar 

  16. C. Calcagno, S. Helsen, and P. Thiemann. Syntactic type soundness results for the region calculus. Information and Computation, to appear 200x.

    Google Scholar 

  17. P. Cenciarelli and E. Moggi. A syntactic approach to modularity in denotational semantics. In CTCS 1993, 1993. CWI Tech. Report.

    Google Scholar 

  18. H. B. Curry. The elimination theorem when modality is present. Journal of Symbolic Logic, 17(4):249–265, January 1957.

    Google Scholar 

  19. O. Danvy and A. Filinski. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science, 2, 1992.

    Google Scholar 

  20. O. Danvy and J. Hatcliff. CPS transformation after strictness analysis. ACM Letters on Programming Languages and Systems, 1(3), 1993.

    Google Scholar 

  21. S. dal Zilio and A. Gordon. Region analysis and a π-calculus with groups. In 25th International Symposium on Mathematical Foundations of Computer Science, August 2000.

    Google Scholar 

  22. A. Filinski. Representing layered monads. In POPL’99. ACM Press, 1999.

    Google Scholar 

  23. M. Fairtlough and M. Mendler. An intuitionistic modal logic with applications to the formal verification of hardware. In Proceedings of Computer Science Logic 1994, volume 933 of Lecture Notes in Computer Science. Springer-Verlag, 1995.

    Chapter  Google Scholar 

  24. C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence of compiling with continuations. In Proceedings of the 1993 Conference on Programming Language Design and Implementation. ACM, 1993.

    Google Scholar 

  25. 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, 1987.

    Google Scholar 

  26. D.K. Gifford and J.M. Lucassen. Integrating functional and imperative programming. In ACM Conference on Lisp and Functional Programming. ACM Press, 1986.

    Google Scholar 

  27. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Number 7 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

    Google Scholar 

  28. M.J.C. Gordon. Denotational Description of Programming Languages. Springer, 1979.

    Google Scholar 

  29. J. Gustavsson and D. Sands. A foundation for space-safe transformations of call-by-need programs. In A. D. Gordon and A. M. Pitts, editors, The Third International Workshop on Higher Order Operational Techniques in Semantics, volume 26 of Electronic Notes in Theoretical Computer Science. Elsevier, 1999.

    Google Scholar 

  30. J. Hatcliff and O. Danvy. A generic account of continuation-passing styles. In Proceedings of the 21st Annual Symposium on Principles of Programming Languages. ACM, January 1994.

    Google Scholar 

  31. Graham Hutton and Erik Meijer. Monadic parsing in Haskell. Journal of Functional Programming, 8(4):437–444, July 1998.

    Google Scholar 

  32. D. J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2):103–112, February 1996.

    Google Scholar 

  33. P. Hudak. Modular domain specific languages and tools. In Fifth International Conference on Software Reuse, pages 134–142, Victoria, Canada, June 1998.

    Google Scholar 

  34. John Hughes. Restricted Datatypes in Haskell. In Third Haskell Workshop. Utrecht University technical report, 1999.

    Google Scholar 

  35. Bart Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, 1999.

    Google Scholar 

  36. Simon Peyton Jones, John Hughes, (editors), Lennart Augustsson, Dave Barton, Brian Boutel, Warren Burton, Joseph Fasel, Kevin Hammond, Ralf Hinze, Paul Hudak, Thomas Johnsson, Mark Jones, John Launchbury, Erik Meijer, John Peterson, Alastair Reid, Colin Runciman, and Philip Wadler. Report on the Programming Language Haskell 98, a Non-strict, Purely Functional Language. Available from http://haskell.org, February 1999.

  37. Simon Peyton Jones. Explicit quantification in Haskell. http://research.microsoft.com/users/simonpj/Haskell/quantification.html.

  38. Mark P Jones, Alastair Reid, the Yale Haskell Group, the Oregon Graduate Institute of Science, and Technology. The Hugs 98 user manual. Available from http://haskell.org/hugs, 1994-1999.

  39. Simon Peyton Jones and Philip Wadler. Imperative functional programming. In 20’th Symposium on Principles of Programming Languages, Charlotte, North Carolina, January 1993. ACM Press.

    Google Scholar 

  40. D. Kranz, R. Kelsey, J. Rees, P. Hudak, J. Philbin, and N. Adams. Orbit: An optimizing compiler for Scheme. In Proceedings of the ACM SIGPLAN Symposium on Compiler Construction, SIGPLAN Notices, pages 219–233, 1986.

    Google Scholar 

  41. D. King and J. Launchbury. Structuring depth-first search algorithms in Haskell. In Conf. Record 22nd Symp. on Principles of Programming Languages, pages 344–354, San Francisco, California, 1995. ACM.

    Google Scholar 

  42. P.B. Levy. Call-by-push-value: a subsuming paradigm (extended abstract). In Typed Lambda-Calculi and Applications, volume 1581 of LNCS. Springer, 1999.

    Chapter  Google Scholar 

  43. S. Liang and P. Hudak. Modular denotational semantics for compiler construction. In ESOP’96, volume 1058 of LNCS. Springer, 1996.

    Google Scholar 

  44. S. Liang, P. Hudak, and M. Jones. Monad transformers and modular interpreters. In POPL’95. ACM Press, 1995.

    Google Scholar 

  45. J. Launchbury and S. Peyton Jones. Lazy functional state threads. In Proceedings of the 1994 SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 1994.

    Google Scholar 

  46. J. Launchbury and A. Sabry. Monadic state: Axiomatisation and type safety. In Proceedings of the International Conference on Functional Programming. ACM, 1997.

    Google Scholar 

  47. X. Leroy and P. Weis. Polymorphic type inference and assignment. In Proceedings of the 1991 ACM Conference on Principles of Programming Languages. ACM, 1991.

    Google Scholar 

  48. E. Manes. Algebraic Theories. Graduate Texts in Mathematics. Springer, 1976.

    Google Scholar 

  49. E Manes. Implementing collection classes with monads. Mathematical Structures in Computer Science, 8(3), 1998.

    Google Scholar 

  50. Y. Minamide. A functional represention of data structures with a hole. In Proceedings of the 25rd Symposium on Principles of Programming Languages, 1998.

    Google Scholar 

  51. Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Conference Record of the 23rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg, Florida. ACM, January 1996.

    Google Scholar 

  52. E. Moggi. Computational lambda-calculus and monads. In Proceedings of the 4th Annual Symposium on Logic in Computer Science, Asiloomar, CA, pages 14–23, 1989.

    Google Scholar 

  53. E. Moggi. Notions of computation and monads. Information and Computation, 93(1), 1991.

    Google Scholar 

  54. E. Moggi. A semantics for evaluation logic. Fundamenta Informaticae, 22(1/2), 1995.

    Google Scholar 

  55. E. Moggi. Metalanguages and applications. In Semantics and Logics of Computation, volume 14 of Publications of the Newton Institute. Cambridge University Press, 1997.

    Google Scholar 

  56. P. Mosses. Denotational semantics. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 11. MIT press, 1990.

    Google Scholar 

  57. P. Mosses. Action Semantics. Number 26 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.

    Google Scholar 

  58. E. Moggi and F. Palumbo. Monadic encapsulation of effects: A revised approach. In Proceedings of the Third International Workshop on Higher-Order Operational Techniques in Semantics, Electronic Notes in Theoretical Computer Science. Elsevier, September 1999.

    Google Scholar 

  59. E. Moggi and A. Sabry. Monadic encapsulation of effects: A revised approach (extended version). Journal of Functional Programming, 11(6), November 2001.

    Google Scholar 

  60. I. Mason and C. Talcott. Equivalences in functional languages with effects. Journal of Functional Programming, 1:287–327, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  61. G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):528–569, May 1999.

    Google Scholar 

  62. F. Nielson and H. R. Nielson. Higher-order concurrent programs with finite communication topology. In Proceedings of the 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1994.

    Google Scholar 

  63. H. R. Nielson, F. Nielson, and T. Amtoft. Polymorphic subtyping for effect analysis: The static semantics. In Mads Dam, editor, Proceedings of the Fifth LOMAPS Workshop, number 1192 in Lecture Notes in Computer Science. Springer-Verlag, 1997.

    Google Scholar 

  64. F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.

    Google Scholar 

  65. F. Pfenning and R. Davies. A judgemental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4), August 2001.

    Google Scholar 

  66. S. L. Peyton Jones. Compiling Haskell by program transformation: A report from the trenches. In Proceedings of the European Symposium on Programming, Linköping, Sweden, number 1058 in Lecture Notes in Computer Science. Springer-Verlag, January 1996.

    Google Scholar 

  67. Simon Peyton Jones. Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. In R Steinbrueggen, editor, Engineering theories of software construction, Marktoberdorf Summer School 2000, NATO ASI Series. IOS Press, 2001.

    Google Scholar 

  68. A. M. Pitts. Operationally-based theories of program equivalence. In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation, Publications of the Newton Institute, pages 241–298. Cambridge University Press, 1997.

    Google Scholar 

  69. A. M. Pitts. Operational semantics and program equivalence. revised version of lectures at the international summer school on applied semantics. This volume, September 2000.

    Google Scholar 

  70. A.M. Pitts. Categorical logic. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 5. Oxford University Press, 2000.

    Google Scholar 

  71. G. D. Plotkin. Call-by-name, call-by-value and the lambda calculus. Theoretical Computer Science, pages 125–159, 1975.

    Google Scholar 

  72. G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

    Article  MathSciNet  Google Scholar 

  73. S. L. Peyton Jones, J. Launchbury, M. B. Shields, and A. P. Tolmach. Bridging the gulf: A common intermediate language for ML and Haskell. In Proceedings of POPL’98. ACM, 1998.

    Google Scholar 

  74. S. L. Peyton Jones, J. Launchbury, M. B. Shields, and A. P. Tolmach. Corrigendum to bridging the gulf: A common intermediate language for ML and Haskell. Available from http://www.cse.ogi.edu/mbs/pub, 1998.

  75. D.S. Scott. A type-theoretic alternative to CUCH, ISWIM, OWHY. Theoretical Computer Science, 121, 1993.

    Google Scholar 

  76. A. Sabry and M. Felleisen. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 6(3/4):289–360, 1993.

    Article  Google Scholar 

  77. Z. Shao. An overview of the FLINT/ML compiler. In Proceedings of the 1997 ACM Workshop on Types in Compilation, Amsterdam. ACM, June 1997.

    Google Scholar 

  78. M. Semmelroth and A. Sabry. Monadic encapsulation in ML. In Proceedings of the International Conference on Functional Programming. ACM, 1999.

    Google Scholar 

  79. I. D. B. Stark. Names and Higher Order Functions. PhD thesis, Computer Laboratory, University of Cambridge, 1994.

    Google Scholar 

  80. I. Stark. Categorical models for local names. Lisp and Symbolic Computation, 9(1), February 1996.

    Google Scholar 

  81. Amr Sabry and Philip Wadler. A reflection on call-by-value. ACM Transactions on Programming Languages and Systems, 19(6):916–941, November 1997.

    Google Scholar 

  82. J.-P. Talpin and P. Jouvelot. The type and effect discipline. Information and Computation, 111(2), June 1994. Revised from LICS 1992.

    Google Scholar 

  83. M. Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, Department of Computer Science, University of Edinburgh, 1987.

    Google Scholar 

  84. A. Tolmach. Optimizing ML using a hierarchy of monadic types. In Proceedings of the Workshop on Types in Compilation, Kyoto, March 1998.

    Google Scholar 

  85. M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2), February 1997.

    Google Scholar 

  86. P. Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2, 1992.

    Google Scholar 

  87. P. Wadler. The essence of functional programming. In Proceedings 1992 Symposium on Principles of Programming Languages, pages 1–14, Albuquerque, New Mexico, 1992.

    Google Scholar 

  88. P. Wadler. Monads for functional programming. In J. Jeuring and E. Meijer, editors, Advanced Functional Programming, number 925 in LNCS, pages 24–52. Springer Verlag, May 1995.

    Google Scholar 

  89. P. Wadler. The marriage of effects and monads. In International Conference on Functional Programming. ACM Press, 1998.

    Google Scholar 

  90. A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 15 November 1994.

    Google Scholar 

  91. A. Wright. Simple imperative polymorphism. LISP and Symbolic Computation, 8:343–355, 1995.

    Article  Google Scholar 

  92. P. Wadler and P. Thiemann. The marriage of effects and monads. To appear in ACM Transactions on Computational Logic, 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, USA

    Nick Benton

  2. Chalmers Univ., Sweden

    John Hughes

  3. DISI, Univ. di Genova, Genova, Italy

    Eugenio Moggi

Authors
  1. Nick Benton
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John Hughes
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Eugenio Moggi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Projet Lemme, INRIA Sophia-Antipolis, 2004 Route des Lucioles, BP 93, 06902, Sophia Antipolis Cedex, France

    Gilles Barthe

  2. Department of Computing Science, Chalmers University of Technology, 412 96, Göteborg, Sweden

    Peter Dybjer

  3. Departamento de Matemática, Universidade do Minho, Campus de Gualtar, 4710-057, Braga, Portugal

    Luís Pinto

  4. Departamento de Informática, Universidade do Minho, Campus de Gualtar, 4710-057, Braga, Portugal

    João Saraiva

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Benton, N., Hughes, J., Moggi, E. (2002). Monads and Effects. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds) Applied Semantics. APPSEM 2000. Lecture Notes in Computer Science, vol 2395. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45699-6_2

Download citation

  • DOI: https://doi.org/10.1007/3-540-45699-6_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44044-4

  • Online ISBN: 978-3-540-45699-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation