Witnessing side effects

ABSTRACT

We present a new approach to the old problem of adding global mutable state to purely functional languages. Our idea is to extend the language with “witnesses,” which is based on an arguably more pragmatic motivation than past approaches. We give a semantic condition for correctness and prove it is sufficient. We also give a somewhat surprising static checking algorithm that makes use of a network flow property equivalent to the semantic condition via reduction to a satisfaction problem for a system of linear inequalities.

REFERENCES

• 1: Peter Achten , John H. G. van Groningen , Rinus Plasmeijer, High Level Specification of I/O in Functional Languages, Proceedings of the 1992 Glasgow Workshop on Functional Programming, p.1-17, July 06-08, 1992
• 2: Zena M. Ariola , Matthias Felleisen, The call-by-need lambda calculus, Journal of Functional Programming, v.7 n.3, p.265-301, May 1997 [doi>10.1017/S0956796897002724]
• 3: Zena M. Ariola , John Maraist , Martin Odersky , Matthias Felleisen , Philip Wadler, A call-by-need lambda calculus, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.233-246, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199507]
• 4: Zena M. Ariola , Amr Sabry, Correctness of monadic state: an imperative call-by-need calculus, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.62-74, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268952]
• 5: Boyland, J. 2003. Checking interference with fractional permissions. In Static Analysis, Tenth International Symposium (San Diego, CA). 55--72.
• 6: Karl Crary , David Walker , Greg Morrisett, Typed memory management in a calculus of capabilities, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.262-275, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292564]
• 7: Manuel Fähndrich , Jeffrey S. Foster , Zhendong Su , Alexander Aiken, Partial online cycle elimination in inclusion constraint graphs, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.85-96, June 17-19, 1998, Montreal, Quebec, Canada
• 8: Dan Grossman , Greg Morrisett , Trevor Jim , Michael Hicks , Yanling Wang , James Cheney, Region-based memory management in cyclone, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 9: Guzman, J. C. and Hudak, P. 1990. Single-threaded polymorphic lambda calculus. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (Philadelphia, PA). IEEE Computer Society Press, Los Alamitos, CA, 42--51.
• 10: John Launchbury, A natural semantics for lazy evaluation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.144-154, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158618]
• 11: John Launchbury , Amr Sabry, Monadic state: axiomatization and type safety, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.227-238, June 09-11, 1997, Amsterdam, The Netherlands
• 12: Matthews, J. and Findler, R. B. 2005. An operational semantics for r5rs scheme. In Proceedings of the 2005 Workshop on Scheme and Functional Programming.
• 13: 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]
• 14: E. Moggi , Amr Sabry, Monadic encapsulation of effects: a revised approach (extended version), Journal of Functional Programming, v.11 n.6, p.591-627, November 2001 [doi>10.1017/S0956796801004154]
• 15: 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]
• 16: 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]
• 17: Plotkin, G. D. 1975. Call-by-name, call-by-value and the lambda-calculus. Theoret. Comput. Sci. 1, 125--159.
• 18: Amr Sabry, What is a purely functional language?, Journal of Functional Programming, v.8 n.1, p.1-22, January 1998 [doi>10.1017/S0956796897002943]
• 19: 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
• 20: Peter Sestoft, Replacing function parameters by global variables, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.39-53, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99374]
• 21: Terauchi, T. and Aiken, A. 2004. Memory management with use-counted regions. Tech. Rep. UCB//CSD-04-1314, University of California, Berkeley, CA. Mar.
• 22: Tachio Terauchi , Alex Aiken, Witnessing side-effects, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 23: Terauchi, T. and Aiken, A. 2006. A capability calculus for concurrency and determinism. In CONCUR 2006—Concurrency Theory, 17th International Conference (Bonn, Germany). 218--232.
• 24: 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]
• 25: David N. Turner , Philip Wadler , Christian Mossin, Once upon a type, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.1-11, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224168]
• 26: Wadler, P. 1990. Linear types can change the world! In IFIP TC 2, Proceedings of the Working Conference on Programming Concepts and Methods (Sea of Galilee, Israel), M. Broy and C. Jones, Eds. North Holland, Amsterdam, The Netherlands, 347--359.
• 27: 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.2 Language Classifications
          Subjects: Applicative (functional) languages

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

Keywords:
Mutable state, side effects