article

Monadic regions

Authors:

Greg MorrisettAuthors Info & Claims

Journal of Functional Programming, Volume 16, Issue 4-5

Pages 485 - 545

https://doi.org/10.1017/S095679680600596X

Published: 01 July 2006 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, and 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 variation of the region calculus of Tofte and Talpin to a monadic variant of System F with region primitives whose types and operations are inspired by (and generalize) the ST monad of Launchbury and Peyton Jones.

References

[1]

Ariola, Zena & Sabry, Amyr (1998) Correctness of monadic state: An imperative call-by-need calculus. Pages 62-74 of: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'98). San Diego, CA: ACM Press.

[2]

Banerjee, Anindya, Heintze, Nevin & Riecke, Jon (1999) Region analysis and the polymorphic lambda calculus. Pages 88-97 of: Proceedings of the 14th IEEE Symposium on Logic in Computer Science (LCS'99). Trento, Italy: IEEE Computer Society Press.

[3]

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

[4]

Calcagno, Cristiano, Helsen, Simon & Thiemann, Peter (2002) Syntactic type soundness results for the region calculus. Information and Computation, 173(2), 199-332.

[5]

Crary, Karl, Walker, David & Morrisett, Greg (1999) Typed memory management in a calculus of capabilities. Pages 262-275 of: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'99). ACM Press.

[6]

Fluet, Matthew (2004) Monadic regions: Formal type soundness and correctness. Tech. rept. TR2004-1936. Department of Computer Science, Cornell University.

[7]

Fluet, Matthew & Morrisett, Greg (2004) Monadic regions. Pages 103-114 of: Proceedings of the 9th ACM SIGPLAN International Conference on Functional Programming (ICFP'04). ACM Press.

[8]

Ganz, Steven E. (forthcoming) Monadic encapsulation of state. PhD thesis, Indiana University, Bloomington, Indiana.

[9]

Girard, Jean-Yves, Taylor, Paul & Lafont, Yves (1989) Proofs and Types. Cambridge University Press.

[10]

Grossman, Dan, Morrisett, Greg, Wang, Yanling, Jim, Trevor, Hicks, Michael & Cheney, James (2001) Formal type soundness for Cyclone's region system. Tech. rept. 2001-1856. Department of Computer Science, Cornell University.

[11]

Grossman, Dan, Morrisett, Greg, Jim, Trevor, Hicks, Michael, Wang, Yanling & Cheney, James (2002) Region-based memory management in Cyclone. Pages 282-293 of: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'02). ACM Press.

[12]

Helsen, Simon & Thiemann, Peter (2000) Syntactic type soundness for the region calculus. Pages 1-19 of: Proceedings of the 4th International Workshop on Higher Order Operational Techniques in Semantics (HOOTS'00). Electronic Notes in Theoretical Computer Science, vol. 41. Montreal, Canada: Elsevier Science Publishers.

[13]

Henglein, Fritz, Makholm, Henning & Niss, Henning (2005) Effect types and region-based memory management. Chap. 3, Pages 87-135 of: Pierce, Benjamin (ed), Advanced Topics in Types and Programming Languages. Cambridge, MA: MIT Press.

[14]

Kagawa, Koji (1997) Compositional references for stateful functional programming. Pages 217-226 of: Proceedings of the 2nd ACM SIGPLAN International Conference on Functional Programming (ICFP'97). ACM Press.

[15]

Kagawa, Koji (2001) Monadic encapsulation with stack of regions. Pages 264-279 of: Proceedings of the 5th International Symposium on Functional and Logic Programming (FLOPS'01). Lecture Notes in Computer Science, vol. 2024. Tokyo, Japan: Springer-Verlag.

[16]

Kieburtz, Richard (1998) Taming effects with monadic typing. Pages 51-62 of: Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP'98). Baltimore, MD: ACM Press.

[17]

Kiselyov, Oleg, Lämmel, Ralf & Schupke, Keean (2004) Strongly typed heterogeneous collections. Pages 96-107 of: Proceedings of the ACM SIGPLAN Workshop on Haskell. ACM Press.

[18]

Launchbury, John & Peyton Jones, Simon (1994) Lazy functional state threads. Pages 24-35 of: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'94). Orlando, FL: ACM Press.

[19]

Launchbury, John & Peyton Jones, Simon (1995) State in Haskell. Lisp and Symbolic Computation, 8(4), 293-341.

Digital Library

[20]

Launchbury, John & Sabry, Amr (1997) Monadic state: Axiomatization and type safety. Pages 227-237 of: Proceedings of the 2nd ACM SIGPLAN International Conference on Functional Programming (ICFP'97). Amsterdam, The Netherlands: ACM Press.

[21]

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

[22]

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

Digital Library

[23]

Moggi, Eugino & Sabry, Amr (2001) Monadic encapsulation of effects: a revised approach (extended version). Journal of Functional Programming, 11(6), 591-627.

Digital Library

[24]

Reynolds, John (1974) Towards a theory of type structure. Pages 408-425 of: Programming symposium. Lecture Notes in Computer Science, vol. 19. Paris, France: Springer-Verlag.

[25]

Riecke, Jon & Viswanathan, Ramesh (1995) Isolating side effects in sequential languages. Pages 1-12 of: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'95). San Francisco, CA: ACM Press.

[26]

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

Digital Library

[27]

Semmelroth, Miley & Sabry, Amr (1999) Monadic encapsulation in ML. Pages 8-17 of: Proceedings of the 4th ACM SIGPLAN International Conference on Functional Programming (ICFP'99). Paris, France: ACM Press.

[28]

Smith, Geoffrey & Volpano, Dennis (1998) A sound polymorphic type system for a dialect of C. Science of Computer Programming, 32(1-3), 49-72.

Digital Library

[29]

Tofte, Mads & Talpin, Jean-Pierre (1994) Implementation of the typed call-by-value ¿-calculus using a stack of regions. Pages 188-201 of: Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'94). Portland, OR: ACM Press.

[30]

Tofte, Mads & Talpin, Jean-Pierre (1997) Region-based memory management. Information and Computation, 132(2), 109-176.

Digital Library

[31]

Tofte, Mads, Birkedal, Lars, Elsman, Martin, Hallenberg, Niels, Olesen, Tommy Højfeld & Sestoft, Peter (2002) Programming with regions in the ML Kit (for version 4). Tech. rept. IT University of Copenhagen.

[32]

Tse, Stephen & Zdancewic, Steve (2004) Translating dependency into parametricity. Pages 115-1125 of: Proceedings of the 9th ACM SIGPLAN International Conference on Functional Programming (ICFP'04). ACM Press.

[33]

Volpano, Dennis & Smith, Geoffrey (1997) Eliminating covert flows with minimum typings. Pages 156-168 of: Proceedings of the 10th IEEE Computer Security Foundations Workshop (CFSW'97). IEEE Computer Society Press.

[34]

Wadler, Philip (1992) The essence of functional programming. Pages 1-14 of: Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'92). ACM Press.

[35]

Wadler, Philip (1995) The marriage of effects and monads. Pages 63-74 of: Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP'98). Baltimore, MD: ACM Press.

[36]

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

Digital Library

[37]

Washburn, Geoffrey & Weirich, Stephanie (2003) Boxes go bannanas: Encoding higher-order abstract syntax with parametric polymorphism. Pages 249-262 of: Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP'03). ACM Press.

Cited By

Bowman W(2024)A Low-Level Look at A-Normal FormProceedings of the ACM on Programming Languages10.1145/36897178:OOPSLA2(165-191)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689717
Kiselyov OIshii H(2015)Freer monads, more extensible effectsACM SIGPLAN Notices10.1145/2887747.280431950:12(94-105)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2887747.2804319
Kiselyov OIshii HLippmeier B(2015)Freer monads, more extensible effectsProceedings of the 2015 ACM SIGPLAN Symposium on Haskell10.1145/2804302.2804319(94-105)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2804302.2804319
Show More Cited By

Monadic regions
1. Theory of computation
  1. Semantics and reasoning

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
ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming

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 ...
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 Journal of Functional Programming

Journal of Functional Programming Volume 16, Issue 4-5

July 2006

285 pages

ISSN:0956-7968

Issue’s Table of Contents

Publisher

Cambridge University Press

United States

Publication History

Published: 01 July 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 09 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Bowman W(2024)A Low-Level Look at A-Normal FormProceedings of the ACM on Programming Languages10.1145/36897178:OOPSLA2(165-191)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689717
Kiselyov OIshii H(2015)Freer monads, more extensible effectsACM SIGPLAN Notices10.1145/2887747.280431950:12(94-105)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2887747.2804319
Kiselyov OIshii HLippmeier B(2015)Freer monads, more extensible effectsProceedings of the 2015 ACM SIGPLAN Symposium on Haskell10.1145/2804302.2804319(94-105)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2804302.2804319
Kameyama YKiselyov OShan C(2015)Combinators for impure yet hygienic code generationScience of Computer Programming10.1016/j.scico.2015.08.007112:P2(120-144)Online publication date: 15-Nov-2015
https://dl.acm.org/doi/10.1016/j.scico.2015.08.007
Yang EMazières D(2014)Dynamic space limits for HaskellACM SIGPLAN Notices10.1145/2666356.259434149:6(588-598)Online publication date: 9-Jun-2014
https://dl.acm.org/doi/10.1145/2666356.2594341
Yang EMazières DO'Boyle MPingali K(2014)Dynamic space limits for HaskellProceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2594291.2594341(588-598)Online publication date: 9-Jun-2014
https://dl.acm.org/doi/10.1145/2594291.2594341
Kameyama YKiselyov OShan C(2011)Shifting the stageJournal of Functional Programming10.1017/S095679681100025621:6(617-662)Online publication date: 1-Nov-2011
https://dl.acm.org/doi/10.1017/S0956796811000256
Charguéraud APottier FHook JThiemann P(2008)Functional translation of a calculus of capabilitiesProceedings of the 13th ACM SIGPLAN international conference on Functional programming10.1145/1411204.1411235(213-224)Online publication date: 20-Sep-2008
https://dl.acm.org/doi/10.1145/1411204.1411235
Charguéraud APottier F(2008)Functional translation of a calculus of capabilitiesACM SIGPLAN Notices10.1145/1411203.141123543:9(213-224)Online publication date: 20-Sep-2008
https://dl.acm.org/doi/10.1145/1411203.1411235
Benton NKennedy ABeringer LHofmann MLeuschel MPodelski A(2007)Relational semantics for effect-based program transformations with dynamic allocationProceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming10.1145/1273920.1273932(87-96)Online publication date: 14-Jul-2007
https://dl.acm.org/doi/10.1145/1273920.1273932

View Options

View options

Figures

Tables

Media

View Issue’s Table of Contents