Article

Monadic regions

Authors:

Greg MorrisettAuthors Info & Claims

ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming

Pages 103 - 114

https://doi.org/10.1145/1016850.1016867

Published: 19 September 2004 Publication History

Abstract

Region-based type systems provide programmer control over memory management without sacrificing type-safety. However, the type systems for region-based languages, such as the ML-Kit or Cyclone, are relatively complicated, so proving their soundness is non-trivial. This paper shows that the complication is in principle unnecessary. In particular, we show that plain old parametric polymorphism, as found in Haskell, is all that is needed. We substantiate this claim by giving a type- and meaning-preserving translation from a region-based language based on core Cyclone to a monadic variant of System F with region primitives whose types and operations are inspired by (and generalize) the ST monad.

References

[1]

Z. Ariola and A. Sabry. Correctness of monadic state: An imperative call-by-need calculus. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'98), pages 62--74. ACM Press, 1998.

Digital Library

[2]

A. Banerjee, N. Heintze, and J. Riecke. Region analysis and the polymorphic lambda calculus. In Proceedings of the 14th IEEE Symposium on Logic in Computer Science (LCS'99), pages 88--97. IEEE Computer Society Press, 1999.

Digital Library

[3]

C. Calcagno. Stratified operational semantics for safety and correctness of the region calculus. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'01), pages 155--165. ACM Press, 2001.

Digital Library

[4]

C. Calcagno, S. Helsen, and P. Thiemann. Syntactic type soundness results for the region calculus. Information and Computation, 173(2):199--332, Mar. 2002.

Digital Library

[5]

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

Digital Library

[6]

M. Fluet. Monadic regions: Formal type soundness and correctness. Technical Report TR2004-1936, Department of Computer Science, Cornell University, Apr. 2004.

[7]

J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge University Press, 1989.

Digital Library

[8]

D. Grossman, G. Morrisett, T. Jim, M. Hicks, Y. Wang, and J. Cheney. Region-based memory management in Cyclone. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'02), pages 282--293. ACM Press, 2002.

Digital Library

[9]

D. Grossman, G. Morrisett, Y. Wang, T. Jim, M. Hicks, and J. Cheney. Formal type soundness for Cyclone's region system. Technical Report 2001-1856, Department of Computer Science, Cornell University, Nov. 2001.

Digital Library

[10]

S. Helsen and P. Thiemann. Syntactic type soundness for the region calculus. In Proceedings of the 4th International Workshop on Higher Order Operational Techniques in Semantics (HOOTS'00), volume 41 of Electronic Notes in Theoretical Computer Science, pages 1--19. Elsevier Science Publishers, Sept. 2000.

[11]

F. Henglein, H. Makholm, and H. Niss. Effect types and region-based memory management. In B. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 5. MIT Press, 2004. In preparation.

[12]

R. Kieburtz. Taming effects with monadic typing. In Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP'98), pages 51--62. ACM Press, 1998.

Digital Library

[13]

O. Kiselyov, R. Lämmel, and K. Schupke. Strongly typed heterogeneous collections, 5 June 2004. Submitted to the Haskell Workshop 2004.

Digital Library

[14]

J. Launchbury and S. Peyton Jones. Lazy functional state threads. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'94), pages 24--35. ACM Press, 1994.

Digital Library

[15]

J. Launchbury and S. Peyton Jones. State in Haskell. Lisp and Symbolic Computation, 8(4):293--341, 1995.

Digital Library

[16]

J. Launchbury and A. Sabry. Monadic state: Axiomatization and type safety. In Proceedings of the 2nd ACMSIGPLAN International Conference on Functional Programming (ICFP'97), pages 227--237. ACM Press, 1997.

Digital Library

[17]

E. Moggi. Computational lambda calculus and monads. In Proceedings of the 4th IEEE Symposium on Logic in Computer Science (LCS'89), pages 14--23, 1989.

Digital Library

[18]

E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55--92, Jan. 1991.

Digital Library

[19]

E. Moggi and A. Sabry. Monadic encapsulation of effects: a revised approach (extended version). Journal of Functional Programming, 11(6):591--627, Nov. 2001.

Digital Library

[20]

J. Reynolds. Towards a theory of type structure. In Programming Symposium, volume 19 of Lecture Notes in Computer Science, pages 408--425. Springer-Verlag, Apr. 1974.

Digital Library

[21]

J. Riecke and R. Viswanathan. Isolating side effects in sequential languages. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'95), pages 1--12. ACM Press, 1995.

Digital Library

[22]

A. Sabry and P. Wadler. A reflection on call-by-value. ACM Transactions on Programming Languages and Systems, 19(6):916--941, Nov. 1997.

Digital Library

[23]

M. Semmelroth and A. Sabry. Monadic encapsulation in ML. In Proceedings of the 4th ACM SIGPLAN International Conference on Functional Programming (ICFP'99), pages 8--17. ACM Press, 1999.

Digital Library

[24]

G. Smith and D. Volpano. A sound polymorphic type system for a dialect of C. Science of Computer Programming, 32(1-3):49--72, 1998.

Digital Library

[25]

M. Tofte, L. Birkedal, M. Elsman, N. Hallenberg, T. H. Olesen, and P. Sestoft. Programming with regions in the ML Kit (for version 4). Technical report, IT University of Copenhagen, Apr. 2002.

[26]

M. Tofte and J.-P. Talpin. Implementation of the typed call-by-value λ -calculus using a stack of regions. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'94), pages 188--201. ACM Press, 1994.

Digital Library

[27]

M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109--176, Feb. 1997.

Digital Library

[28]

D. Volpano and G. Smith. Eliminating covert flows with minimum typings. In Proceedings of the 10th IEEE Computer Security Foundations Workshop (CFSW'97), pages 156--168. IEEE Computer Society Press, 1997.

Digital Library

[29]

P. Wadler. The marriage of effects and monads. In Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP'98), pages 63--74. ACM Press, 1995.

Digital Library

[30]

P. Wadler and P. Thiemann. The marriage of effects and monads. Transactions on Computational Logic, 4(1):1--32, 2003.

Digital Library

Cited By

Elsman M(2024)Explicit Effects and Effect Constraints in ReMLProceedings of the ACM on Programming Languages10.1145/36329218:POPL(2370-2394)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632921
Schuster PBrachthäuser JMüller MOstermann KJhala RDillig I(2022)A typed continuation-passing translation for lexical effect handlersProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523710(566-579)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523710
Schuster PBrachthäuser JOstermann K(2022)Region-based Resource Management and Lexical Exception Handlers in Continuation-Passing StyleProgramming Languages and Systems10.1007/978-3-030-99336-8_18(492-519)Online publication date: 5-Apr-2022
https://dl.acm.org/doi/10.1007/978-3-030-99336-8_18
Show More Cited By

Index Terms

Monadic regions
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
    2. General programming languages
      1. Language features
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Monadic regions
ICFP '04

Region-based type systems provide programmer control over memory management without sacrificing type-safety. However, the type systems for region-based languages, such as the ML-Kit or Cyclone, are relatively complicated, so proving their soundness is ...
Monadic regions

Region-based type systems provide programmer control over memory management without sacrificing type-safety. However, the type systems for region-based languages, such as the ML-Kit or Cyclone, are relatively complicated, and proving their soundness is ...
Lightweight monadic regions
Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell

We present Haskell libraries that statically ensure the safe use of resources such as file handles. We statically prevent accessing an already closed handle or forgetting to close it. The libraries can be trivially extended to other resources such as ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming

September 2004

264 pages

ISBN:1581139055

DOI:10.1145/1016850

General Chair:
Chris Okasaki
United States Military Academy, West Point
,
Program Chair:
Kathleen Fisher
AT&T Labs Research

ACM SIGPLAN Notices Volume 39, Issue 9
ICFP '04
September 2004
254 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1016848
Issue’s Table of Contents

Copyright © 2004 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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 September 2004

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICFP04

Sponsor:

ICFP04: ACM SIGPLAN International Conference on Functional Programming

September 19 - 21, 2004

UT, Snow Bird, USA

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
366
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)1

Reflects downloads up to 09 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Elsman M(2024)Explicit Effects and Effect Constraints in ReMLProceedings of the ACM on Programming Languages10.1145/36329218:POPL(2370-2394)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632921
Schuster PBrachthäuser JMüller MOstermann KJhala RDillig I(2022)A typed continuation-passing translation for lexical effect handlersProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523710(566-579)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523710
Schuster PBrachthäuser JOstermann K(2022)Region-based Resource Management and Lexical Exception Handlers in Continuation-Passing StyleProgramming Languages and Systems10.1007/978-3-030-99336-8_18(492-519)Online publication date: 5-Apr-2022
https://dl.acm.org/doi/10.1007/978-3-030-99336-8_18
Tse SZdancewic S(2019)Translating dependency into parametricityACM SIGPLAN Notices10.1145/1016848.101686839:9(115-125)Online publication date: 27-Feb-2019
https://dl.acm.org/doi/10.1145/1016848.1016868
Kiselyov OShan C(2008)Lightweight monadic regionsACM SIGPLAN Notices10.1145/1543134.141128844:2(1-12)Online publication date: 25-Sep-2008
https://dl.acm.org/doi/10.1145/1543134.1411288
Kiselyov OShan CGill A(2008)Lightweight monadic regionsProceedings of the first ACM SIGPLAN symposium on Haskell10.1145/1411286.1411288(1-12)Online publication date: 25-Sep-2008
https://dl.acm.org/doi/10.1145/1411286.1411288
Goncharov SSchröder LMossakowski T(2006)Completeness of global evaluation logicProceedings of the 31st international conference on Mathematical Foundations of Computer Science10.1007/11821069_39(447-458)Online publication date: 28-Aug-2006
https://dl.acm.org/doi/10.1007/11821069_39
Fluet MMorrisett GAhmed A(2006)Linear regions are all you needProceedings of the 15th European conference on Programming Languages and Systems10.1007/11693024_2(7-21)Online publication date: 27-Mar-2006
https://dl.acm.org/doi/10.1007/11693024_2
Krishnaswami NAldrich JSarkar VHall M(2005)Permission-based ownershipProceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation10.1145/1065010.1065023(96-106)Online publication date: 12-Jun-2005
https://dl.acm.org/doi/10.1145/1065010.1065023
Krishnaswami NAldrich J(2005)Permission-based ownershipACM SIGPLAN Notices10.1145/1064978.106502340:6(96-106)Online publication date: 12-Jun-2005
https://dl.acm.org/doi/10.1145/1064978.1065023
Show More Cited By

View Options

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten