Isolating side effects in sequential languages

ABSTRACT

It is well known that adding side effects to functional languages changes the operational equivalences of the language. We develop a new language construct, encap, that forces imperative pieces of code to behave purely functionally, i.e.,without any visible side effects. The coercion operator encap provides a means of extending the simple reasoning principles for equivalences of code in a functional language to a language with side effects. In earlier work, similar coercion operators were developed, but their correctness required the underlying functional language to include parallel operations. The coercion operators developed here are simpler and are proven correct for purely sequential languages. The sequential setting requires the construction of fully abstract models for sequential call-by-value languages and the formulation of a weak form of “monad” suitable for expressing the semantics of call-by-value languages with side effects.

REFERENCES

• 1: Samson Abramsky, The lazy lambda calculus, Research topics in functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 2: S. Abramsky, R. Jagadeesan, and P. Malacaria. Games and full abstraction for PCF: preliminary announcement. Unpublished, 1993.
• 3: G Berry , P L Curien , J J Lévy, Full abstraction for sequential algorithms: the state of the art, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 4: Robert Cartwright , Matthias Felleisen, Observable sequentiality and full abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.328-342, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143232]
• 5: H. Abelson , R. K. Dybvig , C. T. Haynes , G. J. Rozas , N. I. Adams, IV , D. P. Friedman , E. Kohlbecker , G. L. Steele, Jr. , D. H. Bartley , R. Halstead , D. Oxley , G. J. Sussman , G. Brooks , C. Hanson , K. M. Pitman , M. Wand , William Clinger , Jonathan Rees, Revised report on the algorithmic language scheme, ACM SIGPLAN Lisp Pointers, v.IV n.3, p.1-55, July, 1991 [doi>10.1145/382130.382133]
• 6: P.-L. Curien. Observable sequential algorithms on concrete data structures. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 432-443, 1992.
• 7: Matthias Felleisen, &lgr;-V-CS: an extended &lgr;-calculus for scheme, Proceedings of the 1988 ACM conference on LISP and functional programming, p.72-85, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62686]
• 8: M. Felleisen, The theory and practice of first-class prompts, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.180-190, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73576]
• 9: Carl A. Gunter, Semantics of programming languages: structures and techniques, MIT Press, Cambridge, MA, 1992
• 10: J. C. Guzm~n and A. Su~rez. A type system for exceptions. In Record of the 199'4 A CM SIGPLAN Work.. shop on ML and its Applications, pages 127-135, 1994. Available as INRIA Technical Report 2265.
• 11: Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
• 12: P. Hudak. Continuation-based mutable abstract datatypes, or how to have your state and munge it too. Technical Report Research Report YALEU/DCS/RR- 914, Yale University, 1992.
• 13: P. Hudak, S. L. Peyton Jones, P. L. Wadler, Arvind, B. Boutel, J. Fairbairn, J. Fasel, M. Guzman, K. Hammond, J. Hughes, T. Johnsson, R. Kieburtz, R. S. Nikhil, W. Partain, and J. Peterson. Report on the functional programming language Haskell, Version 1.2. A CM SIGPLAN Notices, May 1992.
• 14: Lorenz Francis Huelsbergen, Dynamic language parallelization, University of Wisconsin at Madison, Madison, WI, 1993
• 15: M. Hyland and L. Ong. Dialogue games and innocent strategies: An approach to intensional full abstraction to PCF (preliminary announcement). Unpublished, 1993.
• 16: P. Jouvelot , D. K. Gifford, Reasoning about continuations with control effects, Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation, p.218-226, June 19-23, 1989, Portland, Oregon, United States
• 17: Pierre Jouvelot , David Gifford, Algebraic reconstruction of types and effects, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.303-310, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99623]
• 18: 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
• 19: J. M. Lucassen. Type.checking Fluent Languages. PhD thesis, Dept. Electrical Engineering & Computer Sci., M#ssachusetts Institute of Technology, 1987. Available as technical report MIT/LCS/TR-408 (MIT Laboratory for Computer Science).
• 20: 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]
• 21: R. Mflner. Fully abstract models of the typed lambda calculus. Theoretical Computer Sci., 4:1-22, 1977.
• 22: R. Mflner. Fully abstract models of the typed lambda Standard ML. MIT Press, 1990.
• 23: 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]
• 24: G. Morrisett. Generalizing first-class stores. In A CM SIGLPLAN Workshop on State #n Programming Languages, p#ges 73-87, 1993. Available as Yale Technical Report YALEU/DCS/RR-968.
• 25: Martin Odersky , Dan Rabin , Paul Hudak, Call by name, assignment, and the lambda calculus, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.43-56, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158521]
• 26: Peter W. O'Hearn , Jon G. Riecke, Kripke logical relations and PCF, Information and Computation, v.120 n.1, p.107-116, July 1995 [doi>10.1006/inco.1995.1103]
• 27: P. W. O'Hearn , R. D. Tennent, Relational parametricity and local variables, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-184, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158624]
• 28: C.-H. L. Ong. The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programruing. PhD thesis, Imperial College, University of London, 1988.
• 29: 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]
• 30: G. D. Plotkin. Call-by-name, call-by-value and the A- calculus. Theoretical Computer Sci., 1:125-159, 1975.
• 31: G. D. Plotkin. LCF considered as # programming language. Theoretical Computer Sci., 5:223-257, 1977.
• 32: John C. Reynolds, Syntactic control of interference, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.39-46, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512766]
• 33: J. C. Reynolds. The essence of Algol. In J. W. de Bakker and J. C. van Vfiet, editors, Algomthmic Languages, pages 345-372. North-Holland, Amsterdam, 1981.
• 34: John C. Reynolds, Syntactic Control of Inference, Part 2, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.704-722, July 11-15, 1989
• 35: Jon Gary Riecke, The logic and expressibility of simply-typed call-by-value and lazy languages, Massachusetts Institute of Technology, Cambridge, MA, 1992
• 36: Jon G. Riecke, Delimiting the scope of effects, Proceedings of the conference on Functional programming languages and computer architecture, p.146-155, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165200]
• 37: Jon G. Riecke, Fully abstract translations between functional languages, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-254, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99617]
• 38: J. G. Riecke and R. Visw#nathan. Full abstraction for call-by-value sequential languages. Unpublished manuscript, 1993.
• 39: Dorai Sitaram , Matthias Felleisen, Reasoning with continuations II: full abstraction for models of control, Proceedings of the 1990 ACM conference on LISP and functional programming, p.161-175, June 27-29, 1990, Nice, France [doi>10.1145/91556.91626]
• 40: Vipin Swarup , Uday S. Reddy , Evan Ireland, Assignments for applicative languages, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.192-214, June 1991, Cambridge, Massachusetts, United States
• 41: J.-P. Talpin. Theoretical and Practical Aspects of Type and Effect Inference. PhD thesis, University of Paris VI, t993.
• 42: J.-P. Talpin and P. Jouvelot. Polymorphic type, region #nd effect inference. Journal of Functional Programming, 2:245-271, 1992.
• 43: 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]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Standard ML

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

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