Document Open Access Logo

Lifting Sequential Effects to Control Operators

Author Colin S. Gordon

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.23.pdf
  • Filesize: 0.65 MB
  • 30 pages

Document Identifiers

Author Details

Colin S. Gordon
  • Drexel University, Philadelphia, PA, USA

Cite AsGet BibTex

Colin S. Gordon. Lifting Sequential Effects to Control Operators. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 23:1-23:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ECOOP.2020.23

Abstract

Sequential effect systems are a class of effect system that exploits information about program order, rather than discarding it as traditional commutative effect systems do. This extra expressive power allows effect systems to reason about behavior over time, capturing properties such as atomicity, unstructured lock ownership, or even general safety properties. While we now understand the essential denotational (categorical) models fairly well, application of these ideas to real software is hampered by the variety of source level control flow constructs and control operators in real languages. We address this new problem by appeal to a classic idea: macro-expression of commonly-used programming constructs in terms of control operators. We give an effect system for a subset of Racket’s tagged delimited control operators, as a lifting of an effect system for a language without direct control operators. This gives the first account of sequential effects in the presence of general control operators. Using this system, we also re-derive the sequential effect system rules for control flow constructs previously shown sound directly, and derive sequential effect rules for new constructs not previously studied in the context of source-level sequential effect systems. This offers a way to directly extend source-level support for sequential effect systems to real programming languages.

Subject Classification

ACM Subject Classification
  • Theory of computation → Semantics and reasoning
  • Theory of computation → Type structures
Keywords
  • Type systems
  • effect systems
  • quantales
  • control operators
  • delimited continuations

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Martin Abadi, Cormac Flanagan, and Stephen N. Freund. Types for safe locking: Static race detection for java. ACM Trans. Program. Lang. Syst., 28(2, //month = mar), 2006. Google Scholar
  2. Martín Abadi and Leslie Lamport. The existence of refinement mappings. In LICS, 1988. Google Scholar
  3. Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253-284, 1991. Google Scholar
  4. Torben Amtoft, Flemming Nielson, and Hanne Riis Nielson. Type and Effect Systems: Behaviours for Concurrency. Imperial College Press, London, UK, 1999. Google Scholar
  5. Kenichi Asai and Yukiyoshi Kameyama. Polymorphic delimited continuations. In APLAS, pages 239-254, 2007. Google Scholar
  6. Robert Atkey. Parameterised Notions of Computation. Journal of Functional Programming, 19:335-376, July 2009. Google Scholar
  7. Andrej Bauer and Matija Pretnar. An effect system for algebraic effects and handlers. In International Conference on Algebra and Coalgebra in Computer Science, pages 1-16. Springer, 2013. Google Scholar
  8. Garrett Birkhoff. Lattice theory, volume 25 of Colloquium Publications. American Mathematical Soc., 1940. Third edition, eighth printing with corrections, 1995. Google Scholar
  9. Thomas Scott Blyth. Lattices and ordered algebraic structures. Springer Science & Business Media, 2006. Google Scholar
  10. Chandrasekhar Boyapati, Robert Lee, and Martin Rinard. Ownership Types for Safe Programming: Preventing Data Races and Deadlocks. In OOPSLA, 2002. Google Scholar
  11. Chandrasekhar Boyapati and Martin Rinard. A Parameterized Type System for Race-Free Java Programs. In OOPSLA, 2001. Google Scholar
  12. Edwin Brady. Programming and reasoning with algebraic effects and dependent types. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP '13, pages 133-144. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500581.
  13. John Clements, Matthew Flatt, and Matthias Felleisen. Modeling an algebraic stepper. In European symposium on programming, pages 320-334. Springer, 2001. Google Scholar
  14. Christopher Coyle and Peter Crogono. Building abstract iterators using continuations. SIGPLAN Not., 26(2):17-24, January 1991. URL: https://doi.org/10.1145/122179.122181.
  15. Olivier Danvy. An analytical approach to program as data objects, 2006. DSc thesis, Department of Computer Science, Aarhus University. Google Scholar
  16. Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. Technical report, DIKU - Computer Science Department, University of Copenhagen, July 1989. Google Scholar
  17. Germán Andrés Delbianco and Aleksandar Nanevski. Hoare-style reasoning with (algebraic) continuations. In ICFP, 2013. Google Scholar
  18. Stephen Dolan, Spiros Eliopoulos, Daniel Hillerström, Anil Madhavapeddy, K. C. Sivaramakrishnan, and Leo White. Concurrent system programming with effect handlers. In Meng Wang and Scott Owens, editors, Trends in Functional Programming, pages 98-117, Cham, 2018. Springer International Publishing. Google Scholar
  19. Matthias Felleisen. The theory and practice of first-class prompts. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988, pages 180-190, 1988. URL: https://doi.org/10.1145/73560.73576.
  20. Matthias Felleisen. On the expressive power of programming languages. Science of computer programming, 17(1-3):35-75, 1991. Google Scholar
  21. Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. Semantics engineering with PLT Redex. Mit Press, 2009. Google Scholar
  22. Matthias Felleisen and Daniel P. Friedman. A reduction semantics for imperative higher-order languages. In PARLE, Parallel Architectures and Languages Europe, Volume II: Parallel Languages, Eindhoven, The Netherlands, June 15-19, 1987, Proceedings, pages 206-223, 1987. URL: https://doi.org/10.1007/3-540-17945-3_12.
  23. Cormac Flanagan and Martín Abadi. Object Types against Races. In CONCUR, 1999. Google Scholar
  24. Cormac Flanagan and Martín Abadi. Types for Safe Locking. In ESOP, 1999. Google Scholar
  25. Cormac Flanagan and Shaz Qadeer. A type and effect system for atomicity. In PLDI, 2003. Google Scholar
  26. Cormac Flanagan and Shaz Qadeer. Types for atomicity. In TLDI, 2003. Google Scholar
  27. Matthew Flatt, Gang Yu, Robert Bruce Findler, and Matthias Felleisen. Adding delimited and composable control to a production programming environment. In ICFP, 2007. Google Scholar
  28. Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control. Proc. ACM Program. Lang., 1(ICFP):13:1-13:29, August 2017. URL: https://doi.org/10.1145/3110257.
  29. Laszlo Fuchs. Partially ordered algebraic systems, volume 28 of International Series of Monographs on Pure and Applied Mathematics. Dover Publications, 2011. Reprint of 1963 Pergamon Press version. Google Scholar
  30. Colin S. Gordon. A Generic Approach to Flow-Sensitive Polymorphic Effects. In ECOOP, 2017. Google Scholar
  31. Colin S. Gordon. Polymorphic Iterable Sequential Effect Systems. Technical Report arXiv cs.PL/cs.LO 1808.02010, Computing Research Repository (Corr), August 2018. In Submission.. URL: http://arxiv.org/abs/1808.02010.
  32. Colin S. Gordon. Sequential Effect Systems with Control Operators. Technical Report arXiv cs.PL 1811.12285, Computing Research Repository (CoRR), December 2018. URL: http://arxiv.org/abs/1811.12285.
  33. Colin S. Gordon, Werner Dietl, Michael D. Ernst, and Dan Grossman. JavaUI: Effects for Controlling UI Object Access. In ECOOP, 2013. Google Scholar
  34. Colin S. Gordon, Michael D. Ernst, and Dan Grossman. Static Lock Capabilities for Deadlock Freedom. In TLDI, 2012. Google Scholar
  35. James Gosling, Bill Joy, Guy L Steele, Gilad Bracha, and Alex Buckley. The Java Language Specification: Java SE 8 Edition. Pearson Education, 2014. Google Scholar
  36. OpenJDK HotSpot Group. OpenJDK Project Loom: Fibers and Continuations, 2019. URL: https://wiki.openjdk.java.net/display/loom/Main.
  37. Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. The Essence of JavaScript. In ECOOP, 2010. Google Scholar
  38. Christopher T. Haynes and Daniel P. Friedman. Embedding continuations in procedural objects. ACM Trans. Program. Lang. Syst., 9(4):582-598, October 1987. URL: https://doi.org/10.1145/29873.30392.
  39. Christopher T. Haynes, Daniel P. Friedman, and Mitchell Wand. Continuations and coroutines. In LISP and Functional Programming, pages 293-298, 1984. Google Scholar
  40. Christopher T. Haynes, Daniel P. Friedman, and Mitchell Wand. Obtaining coroutines with continuations. Comput. Lang., 11(3/4):143-153, 1986. URL: https://doi.org/10.1016/0096-0551(86)90007-X.
  41. P. Jouvelot and D. K. Gifford. Reasoning about continuations with control effects. In PLDI, 1989. Google Scholar
  42. Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. In POPL, 2014. Google Scholar
  43. Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler. Run your research: On the effectiveness of lightweight mechanization. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '12, pages 285-296, New York, NY, USA, 2012. ACM. URL: https://doi.org/10.1145/2103656.2103691.
  44. Ikuo Kobori, Yukiyoshi Kameyama, and Oleg Kiselyov. Answer-type modification without tears: Prompt-passing style translation for typed delimited-control operators. In Olivier Danvy and Ugo de'Liguoro, editors, Proceedings of the Workshop on Continuations, WoC 2016, London, UK, April 12th 2015, volume 212 of EPTCS, pages 36-52, 2015. URL: https://doi.org/10.4204/EPTCS.212.3.
  45. Eric Koskinen and Tachio Terauchi. Local temporal reasoning. In CSL/LICS, 2014. Google Scholar
  46. Shriram Krishnamurthi, Peter Walton Hopkins, Jay A. McCarthy, Paul T. Graunke, Greg Pettyjohn, and Matthias Felleisen. Implementation and use of the PLT scheme web server. Higher-Order and Symbolic Computation, 20(4):431-460, 2007. URL: https://doi.org/10.1007/s10990-007-9008-y.
  47. Daan Leijen. Koka: Programming with Row Polymorphic Effect Types. In Proceedings 5th Workshop on Mathematically Structured Functional Programming (MSFP), 2014. Google Scholar
  48. Daan Leijen. Structured asynchrony with algebraic effects. In Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development, TyDe 2017, pages 16-29, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3122975.3122977.
  49. Sam Lindley and James Cheney. Row-based effect types for database integration. In Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation, pages 91-102. ACM, 2012. Google Scholar
  50. J. M. Lucassen and D. K. Gifford. Polymorphic Effect Systems. In POPL, 1988. Google Scholar
  51. Daniel Marino and Todd Millstein. A Generic Type-and-Effect System. In TLDI, 2009. URL: https://doi.org/10.1145/1481861.1481868.
  52. Microsoft. C#Language Specification: Enumerable Objects, 2018. URL: https://github.com/dotnet/csharplang/blob/master/spec/classes.md#enumerable-objects.
  53. Microsoft. C#Reference: yield Exception Handling, 2018. URL: https://docs.microsoft.com/en-us/dotnet/csharp/language-reference/keywords/yield#exception-handling.
  54. Mozilla. Mozilla Developer Network Documentation: function*, 2018. URL: https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Statements/function*.
  55. Alan Mycroft, Dominic Orchard, and Tomas Petricek. Effect systems revisited - control-flow algebra and semantics. In Semantics, Logics, and Calculi. Springer, 2016. Google Scholar
  56. Iulian Neamtiu, Michael Hicks, Jeffrey S Foster, and Polyvios Pratikakis. Contextual effects for version-consistent dynamic software updating and safe concurrent programming. In POPL, pages 37-49, 2008. Google Scholar
  57. Flemming Nielson and Hanne Riis Nielson. From cml to process algebras. In CONCUR, 1993. Google Scholar
  58. Tomas Petricek, Dominic Orchard, and Alan Mycroft. Coeffects: A calculus of context-dependent computation. In ICFP, 2014. Google Scholar
  59. Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. Typed equivalence of effect handlers and delimited control. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. Google Scholar
  60. Gordon Plotkin and Matija Pretnar. Handlers of algebraic effects. In European Symposium on Programming, pages 80-94. Springer, 2009. Google Scholar
  61. Justin Pombrio and Shriram Krishnamurthi. Inferring type rules for syntactic sugar. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pages 812-825, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3192366.3192398.
  62. Matija Pretnar and Andrej Bauer. An effect system for algebraic effects and handlers. Logical Methods in Computer Science, 10, 2014. Google Scholar
  63. Chung-chieh Shan. A static simulation of dynamic delimited control. Higher-Order and Symbolic Computation, 20(4):371-401, 2007. Google Scholar
  64. Dorai Sitaram. Handling control. In PLDI, 1993. Google Scholar
  65. Dorai Sitaram and Matthias Felleisen. Control delimiters and their hierarchies. Lisp and Symbolic Computation, 3(1):67-99, 1990. Google Scholar
  66. Dorai Sitaram and Matthias Felleisen. Reasoning with continuations II: full abstraction for models of control. In LISP and Functional Programming, pages 161-175, 1990. URL: https://doi.org/10.1145/91556.91626.
  67. Christian Skalka. Types and trace effects for object orientation. Higher-Order and Symbolic Computation, 21(3):239-282, 2008. Google Scholar
  68. Christian Skalka, Scott Smith, and David Van Horn. Types and trace effects of higher order programs. Journal of Functional Programming, 18(2), 2008. Google Scholar
  69. Kohei Suenaga. Type-based deadlock-freedom verification for non-block-structured lock primitives and mutable references. In APLAS, 2008. Google Scholar
  70. Ross Tate. The sequential semantics of producer effect systems. In POPL, 2013. Google Scholar
  71. Python Development Team. Python Enhancement Proposal 255: Simple Generators, 2001. URL: https://www.python.org/dev/peps/pep-0255/.
  72. Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Information and computation, 132(2):109-176, 1997. Google Scholar
  73. Jesse A. Tov and Riccardo Pucella. A theory of substructural types and control. In OOPSLA, 2011. Google Scholar
  74. Philip Wadler and Peter Thiemann. The Marriage of Effects and Monads. Transactions on Computational Logic (TOCL), 4:1-32, 2003. Google Scholar
  75. Mitchell Wand. Type inference for record concatenation and multiple inheritance. In Logic in Computer Science, 1989. LICS'89, Proceedings., Fourth Annual Symposium on, pages 92-97. IEEE, 1989. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact