Taming effects with monadic typing

ABSTRACT

The familiar Hindley-Milner type system of the ML language family is extended with monad annotations to account for possible side effects of expression evaluation. This also allows effects to be effectively encapsulated by lexical scopes Γ with enforcement provided by type checking. A type-and-effects analysis supports type inference. Type soundness and completeness theorems establish the coherence of monadic type inference with the reference semantics of a small ML-style language.

REFERENCES

• AFL95: Alexander Aiken , Manuel Fähndrich , Raph Levien, Better static memory management: improving region-based analysis of higher-order languages, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.174-185, June 18-21, 1995, La Jolla, California, United States
• BTV96: Lars Birkedal , Mads Tofte , Magnus Vejlstrup, From region inference to von Neumann machines via region representation inference, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237771]
• DGT96: O. DanvyFR. GlfickFand P. ThiemannFeditors. Partial Evaluation. Dagstuhl Castle, Germany, February 1996F volume 1110 of Lecture Notes in Computer Science. Berlin: Springer- VerlagF 1996.
• DM82: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• JD94: Mark Jones and Luc Duponcheel. Composing monads. Technical Report YALEU/DCS/RR-1004F Yale UniversityF December 1994.
• LeR98: Xavier LeRoy. Static debugging of uncaught exceptions in ML. Technical reportF IFIP Working Group 2.8 meetingFMarch 1998.
• LP95: John Launchbury , Simon L. Peyton Jones, State in Haskell, Lisp and Symbolic Computation, v.8 n.4, p.293-341, Dec. 1995 [doi>10.1007/BF01018827]
• MTH90: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• MTM97: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• Tal93: J.-P. Talpin. Theoretical and Practical Aspects of Type and Effect Inference. PhD thesisFUniversity of Paris VIF1993.
• TJ92: J.-P. Talpin and P. Jouvelot. Polymorphic typesFregion and effect inference. Journal of Functional ProgrammingF2:245-271F1992.
• Tof87: Mads Tofte. Operationalsemantics andpolymorphic type inference. PhD thesisFUniversity of EdinburghF1987.
• 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
• TT97: Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613 ]
• 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]
• Wad98: 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
• 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:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: ML

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

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