research-article

Open access

Witnessing side effects

Authors:

Tachio Terauchi,

Alex AikenAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 30, Issue 3

Article No.: 15, Pages 1 - 42

https://doi.org/10.1145/1353445.1353449

Published: 21 May 2008 Publication History

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]

Achten, P., van Groningen, J. H. G., and Plasmeijer, R. 1993. High level specification of I/O in functional languages. In Proceedings of the 1992 Glasgow Workshop on Functional Programming. Springer-Verlag, New York, 1--17.

Digital Library

[2]

Ariola, Z. M. and Felleisen, M. 1997. The call-by-need lambda calculus. J. Funct. Prog. 7, 3, 265--301.

Digital Library

[3]

Ariola, Z. M., Maraist, J., Odersky, M., Felleisen, M., and Wadler, P. 1995. A call-by-need lambda calculus. In Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Francisco, CA). ACM, New York, 233--246.

Digital Library

[4]

Ariola, Z. M. and Sabry, A. 1998. Correctness of monadic state: an imperative call-by-need calculus. In Proceedings of the 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Diego, CA). 62--74.

Digital Library

[5]

Boyland, J. 2003. Checking interference with fractional permissions. In Static Analysis, Tenth International Symposium (San Diego, CA). 55--72.

Digital Library

[6]

Crary, K., Walker, D., and Morrisett, G. 1999. Typed memory management in a calculus of capabilities. In Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Antonio, TX). 262--275.

Digital Library

[7]

Fähndrich, M., Foster, J. S., Su, Z., and Aiken, A. 1998. Partial online cycle elimination in inclusion constraint graphs. In Proceedings of the 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation (Montreal, Ont., Canada). ACM, New York, 85--96.

Digital Library

[8]

Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., and Cheney, J. 2002. Region-based memory management in Cyclone. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (Berlin, Germany). ACM, New York.

Digital Library

[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]

Launchbury, J. 1993. A natural semantics for lazy evaluation. In Proceedings of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Charleston, SC). ACM, New York, 144--154.

Digital Library

[11]

Launchbury, J. and Sabry, A. 1997. Monadic state: Axiomatization of type safety. In Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (Amsterdam, The Netherlands). ACM, New York, 227--238.

Digital Library

[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]

Moggi, E. 1991. Notions of computation and monads. Inf. Comput. 93, 1, 55--92.

Digital Library

[14]

Moggi, E. and Sabry, A. 2001. Monadic encapsulation of effects: a revised approach (extended version). J. Funct. Prog. 11, 6, 591--627.

Digital Library

[15]

Odersky, M., Rabin, D., and Hudak, P. 1993. Call by name, assignment, and the lambda calculus. In Proceedings of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Charleston, SC). ACM, New York, 43--56.

Digital Library

[16]

Peyton Jones, S. L. and Wadler, P. 1993. Imperative functional programming. In Proceedings of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Charleston, SC). ACM, New York, 71--84.

Digital Library

[17]

Plotkin, G. D. 1975. Call-by-name, call-by-value and the lambda-calculus. Theoret. Comput. Sci. 1, 125--159.

[18]

Sabry, A. 1998. What is a purely functional language&quest; J. Funct. Prog. 8, 1, 1--22.

Digital Library

[19]

Semmelroth, M. and Sabry, A. 1999. Monadic encapsulation in ml. In Proceedings of the 4th ACM SIGPLAN International Conference on Functional Programming (Paris, France). ACM, New York, 8--17.

Digital Library

[20]

Sestoft, P. 1989. Replacing function parameters by global variables. In FPCA '89 Conference on Functional Programming Languages and Computer Architecture (London, United Kingdom).

Digital Library

[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]

Terauchi, T. and Aiken, A. 2005. Witnessing side-effects. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (Tallinn, Estonia). ACM, New York, 105--115.

Digital Library

[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.

Digital Library

[24]

Tofte, M. and Talpin, J.-P. 1994. Implementation of the typed call-by-value λ-calculus using a stack of regions. In Proceedings of the 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Portland, OR). ACM, New York, 188--201.

Digital Library

[25]

Turner, D. N., Wadler, P., and Mossin, C. 1995. Once upon a type. In FPCA '95 Conference on Functional Programming Languages and Computer Architecture (La Jolla, CA), 1--11.

Digital Library

[26]

Wadler, P. 1990. Linear types can change the world&excl; 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]

Wright, A. K. and Felleisen, M. 1994. A syntactic approach to type soundness. Inf. Comput. 115, 1, 38--94.

Digital Library

Cited By

Westrick SArora JAcar U(2022)Entanglement detection with near-zero costProceedings of the ACM on Programming Languages10.1145/35476466:ICFP(679-710)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547646
Arora JWestrick SAcar U(2021)Provably space-efficient parallel functional programmingProceedings of the ACM on Programming Languages10.1145/34342995:POPL(1-33)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434299
Westrick SYadav RFluet MAcar U(2019)Disentanglement in nested-parallel programsProceedings of the ACM on Programming Languages10.1145/33711154:POPL(1-32)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371115
Show More Cited By

Index Terms

Witnessing side effects
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages
2. Theory of computation
  1. Semantics and reasoning

Recommendations

Witnessing side-effects
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

We present a new approach to the old problem of adding side effects 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 ...
Witnessing side-effects
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

We present a new approach to the old problem of adding side effects 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 ...
Epistemic Side Effects: An AI Safety Problem
AAMAS '23: Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems

AI safety research has investigated the problem of negative side effects -- undesirable changes made by AI systems in pursuit of an underspecified objective. However, the focus has been on physical side effects, such as a robot breaking a vase while ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 30, Issue 3

May 2008

245 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/1353445

Issue’s Table of Contents

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 May 2008

Accepted: 01 May 2007

Revised: 01 January 2007

Received: 01 April 2006

Published in TOPLAS Volume 30, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
491
Total Downloads

Downloads (Last 12 months)60
Downloads (Last 6 weeks)14

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Westrick SArora JAcar U(2022)Entanglement detection with near-zero costProceedings of the ACM on Programming Languages10.1145/35476466:ICFP(679-710)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547646
Arora JWestrick SAcar U(2021)Provably space-efficient parallel functional programmingProceedings of the ACM on Programming Languages10.1145/34342995:POPL(1-33)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434299
Westrick SYadav RFluet MAcar U(2019)Disentanglement in nested-parallel programsProceedings of the ACM on Programming Languages10.1145/33711154:POPL(1-32)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371115
Muller SChong S(2012)Towards a practical secure concurrent languageACM SIGPLAN Notices10.1145/2398857.238462147:10(57-74)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2398857.2384621
Muller SChong SLeavens GDwyer M(2012)Towards a practical secure concurrent languageProceedings of the ACM international conference on Object oriented programming systems languages and applications10.1145/2384616.2384621(57-74)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2384616.2384621
Goto MJagadeesan RPtcher CRiely JPierce B(2012)Types for relaxed memory modelsProceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation10.1145/2103786.2103791(25-38)Online publication date: 28-Jan-2012
https://dl.acm.org/doi/10.1145/2103786.2103791
Outman SMcGregor J(2009)Identifying task-level parallelism by functional transformation with side-effect domainsProceedings of the 47th annual ACM Southeast Conference10.1145/1566445.1566482(1-6)Online publication date: 19-Mar-2009
https://dl.acm.org/doi/10.1145/1566445.1566482
Herhut SScholz SGrelck CPetersen LChakravarty M(2009)Controlling chaosProceedings of the 4th workshop on Declarative aspects of multicore programming10.1145/1481839.1481847(59-67)Online publication date: 20-Jan-2009
https://dl.acm.org/doi/10.1145/1481839.1481847

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents