Document Open Access Logo

A Generic Approach to Flow-Sensitive Polymorphic Effects

Author Colin S. Gordon

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2017.13.pdf
  • Filesize: 0.79 MB
  • 31 pages

Document Identifiers

Author Details

Colin S. Gordon

Cite AsGet BibTex

Colin S. Gordon. A Generic Approach to Flow-Sensitive Polymorphic Effects. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 13:1-13:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ECOOP.2017.13

Abstract

Effect systems are lightweight extensions to type systems that can verify a wide range of important properties with modest developer burden. But our general understanding of effect systems is limited primarily to systems where the order of effects is irrelevant. Understanding such systems in terms of a lattice of effects grounds understanding of the essential issues, and provides guidance when designing new effect systems. By contrast, sequential effect systems --- where the order of effects is important --- lack a clear algebraic characterization. We derive an algebraic characterization from the shape of prior concrete sequential effect systems. We present an abstract polymorphic effect system with singleton effects parameterized by an effect quantale --- an algebraic structure with well-defined properties that can model a range of existing order-sensitive effect systems. We define effect quantales, derive useful properties, and show how they cleanly model a variety of known sequential effect systems. We show that effect quantales provide a free, general notion of iterating a sequential effect, and that for systems we consider the derived iteration agrees with the manually designed iteration operators in prior work. Identifying and applying the right algebraic structure led us to subtle insights into the design of order-sensitive effect systems, which provides guidance on non-obvious points of designing order-sensitive effect systems. Effect quantales have clear relationships to the recent category theoretic work on order-sensitive effect systems, but are explained without recourse to category theory. In addition, our derived iteration construct should generalize to these semantic structures, addressing limitations of that work.
Keywords
  • Type systems
  • effect systems
  • quantales
  • polymorphism

Metrics

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

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):207-255, March 2006. URL: http://dx.doi.org/10.1145/1119479.1119480.
  2. Samson Abramsky and Steven Vickers. Quantales, observational logic and process semantics. Mathematical Structures in Computer Science, 3(02):161-227, 1993. URL: http://dx.doi.org/10.1017/S0960129500000189.
  3. Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. A theory of gradual effect systems. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP '14, pages 283-295. ACM, 2014. URL: http://dx.doi.org/10.1145/2628136.2628149.
  4. Nick Benton and Peter Buchlovsky. Semantics of an Effect Analysis for Exceptions. In TLDI, 2007. URL: http://dx.doi.org/10.1145/1190315.1190320.
  5. Lars Birkedal and Rasmus Ejlers Møgelberg. Intensional type theory with guarded recursive types qua fixed points on universes. In Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on, pages 213-222. IEEE, 2013. URL: http://dx.doi.org/10.1109/LICS.2013.27.
  6. Garrett Birkhoff. Lattice theory, volume 25 of Colloquium Publications. American Mathematical Soc., 1940. Third edition, eighth printing with corrections, 1995. Google Scholar
  7. Thomas Scott Blyth. Lattices and ordered algebraic structures. Springer Science &Business Media, 2006. URL: http://dx.doi.org/10.1007/b139095.
  8. Robert L. Bocchino, Jr., Vikram S. Adve, Danny Dig, Sarita V. Adve, Stephen Heumann, Rakesh Komuravelli, Jeffrey Overbey, Patrick Simmons, Hyojin Sung, and Mohsen Vakilian. A Type and Effect System for Deterministic Parallel Java. In OOPSLA, 2009. URL: http://dx.doi.org/10.1145/1640089.1640097.
  9. Chandrasekhar Boyapati, Robert Lee, and Martin Rinard. Ownership Types for Safe Programming: Preventing Data Races and Deadlocks. In OOPSLA, 2002. URL: http://dx.doi.org/10.1145/582419.582440.
  10. Chandrasekhar Boyapati and Martin Rinard. A Parameterized Type System for Race-Free Java Programs. In OOPSLA, 2001. URL: http://dx.doi.org/10.1145/504282.504287.
  11. Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 262-275. ACM, 1999. URL: http://dx.doi.org/10.1145/292540.292564.
  12. Benjamin Delaware, Bruno C. d. S. Oliveira, and Tom Schrijvers. Meta-theory à la carte. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pages 207-218. ACM, 2013. URL: http://dx.doi.org/10.1145/2429069.2429094.
  13. Benjamin Delaware, Steven Keuchel, Tom Schrijvers, and Bruno C.d.S. Oliveira. Modular monadic meta-theory. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP '13, pages 319-330. ACM, 2013. URL: http://dx.doi.org/10.1145/2500365.2500587.
  14. Mike Dodds, Xinyu Feng, Matthew Parkinson, and Viktor Vafeiadis. Deny-guarantee reasoning. In Proceedings of the 18th European Symposium on Programming (ESOP), pages 363-377. Springer Berlin Heidelberg, 2009. URL: http://dx.doi.org/10.1007/978-3-642-00590-9_26.
  15. Peter Dybjer. Internal type theory. In International Workshop on Types for Proofs and Programs, pages 120-134. Springer, 1995. URL: http://dx.doi.org/10.1007/3-540-61780-9_66.
  16. Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, James R. Larus, and Steven Levi. Language support for fast and reliable message-based communication in singularity os. In Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006, EuroSys '06, pages 177-190. ACM, 2006. URL: http://dx.doi.org/10.1145/1217935.1217953.
  17. Cormac Flanagan and Martín Abadi. Object Types against Races. In CONCUR, 1999. URL: http://dx.doi.org/10.1007/3-540-48320-9_21.
  18. Cormac Flanagan and Martín Abadi. Types for Safe Locking. In ESOP, 1999. URL: http://dx.doi.org/10.1007/3-540-49099-X_7.
  19. Cormac Flanagan and Stephen N. Freund. Type-Based Race Detection for Java. In PLDI, 2000. URL: http://dx.doi.org/10.1145/349299.349328.
  20. Cormac Flanagan and Shaz Qadeer. A type and effect system for atomicity. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, PLDI '03, pages 338-349. ACM, 2003. URL: http://dx.doi.org/10.1145/781131.781169.
  21. Cormac Flanagan and Shaz Qadeer. Types for atomicity. In Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, TLDI '03, pages 1-12. ACM, 2003. URL: http://dx.doi.org/10.1145/604174.604176.
  22. 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
  23. Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono. Residuated lattices: an algebraic glimpse at substructural logics, volume 151 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2007. Google Scholar
  24. Ronald Garcia, Éric Tanter, Roger Wolff, and Jonathan Aldrich. Foundations of typestate-oriented programming. ACM Trans. Program. Lang. Syst., 36(4):12:1-12:44, October 2014. URL: http://dx.doi.org/10.1145/2629609.
  25. David K. Gifford and John M. Lucassen. Integrating Functional and Imperative Programming. In Proceedings of the 1986 ACM Conference on LISP and Functional Programming, LFP '86, 1986. URL: http://dx.doi.org/10.1145/319838.319848.
  26. Colin S. Gordon. A Generic Approach to Flow-Sensitive Polymorphic Effects (Extended Version). Technical Report arXiv cs.PL 1705.02264, Computing Research Repository (CoRR), May 2017. URL: https://arxiv.org/abs/1705.02264.
  27. Colin S. Gordon, Werner Dietl, Michael D. Ernst, and Dan Grossman. JavaUI: Effects for Controlling UI Object Access. In Proceedings of the 27th European Conference on Object-Oriented Programming (ECOOP'13), 2013. URL: http://dx.doi.org/10.1007/978-3-642-39038-8_8.
  28. Colin S. Gordon, Michael D. Ernst, and Dan Grossman. Static Lock Capabilities for Deadlock Freedom. In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'12), 2012. URL: http://dx.doi.org/10.1145/2103786.2103796.
  29. 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
  30. Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. Region-based memory management in cyclone. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, PLDI '02, pages 282-293. ACM, 2002. URL: http://dx.doi.org/10.1145/512529.512563.
  31. Fritz Henglein, Henning Makholm, and Henning Niss. Effect types and region-based memory management. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 3, pages 87-136. MIT Press, 2005. Google Scholar
  32. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous Session Types. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '08, 2008. URL: http://dx.doi.org/10.1145/1328438.1328472.
  33. Galen Hunt, Mark Aiken, Manuel Fähndrich, Chris Hawblitzel, Orion Hodson, James Larus, Steven Levi, Bjarne Steensgaard, David Tarditi, and Ted Wobber. Sealing os processes to improve dependability and safety. In Proceedings of the 2Nd ACM SIGOPS/EuroSys European Conference on Computer Systems 2007, EuroSys '07, pages 341-354. ACM, 2007. URL: http://dx.doi.org/10.1145/1272996.1273032.
  34. Galen C. Hunt and James R. Larus. Singularity: Rethinking the software stack. SIGOPS Oper. Syst. Rev., 41(2):37-49, April 2007. URL: http://dx.doi.org/10.1145/1243418.1243424.
  35. Bart Jacobs. Categorical logic and type theory, volume 141 of Studies in Logic and the Foundations of Mathematics. Elsevier, 1999. Google Scholar
  36. Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 633-645. ACM, 2014. URL: http://dx.doi.org/10.1145/2535838.2535846.
  37. Ming Kawaguchi, Patrick Rondon, Alexander Bakst, and Ranjit Jhala. Deterministic Parallelism via Liquid Effects. In PLDI, 2012. URL: http://dx.doi.org/10.1145/2254064.2254071.
  38. Eric Koskinen and Tachio Terauchi. Local temporal reasoning. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, pages 59:1-59:10, New York, NY, USA, 2014. ACM. URL: http://dx.doi.org/10.1145/2603088.2603138.
  39. Dexter Kozen. Kleene algebra with tests. ACM Transactions on Programming Languages and Systems (TOPLAS), 19(3):427-443, 1997. URL: http://dx.doi.org/10.1145/256167.256195.
  40. Richard J. Lipton. Reduction: A Method of Proving Properties of Parallel Programs. Communications of the ACM, 18(12):717-721, December 1975. URL: http://dx.doi.org/10.1145/361227.361234.
  41. J. M. Lucassen and D. K. Gifford. Polymorphic Effect Systems. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 1988. URL: http://dx.doi.org/10.1145/73560.73564.
  42. Daniel Marino and Todd Millstein. A Generic Type-and-Effect System. In TLDI, 2009. URL: http://dx.doi.org/10.1145/1481861.1481868.
  43. Christopher J. Mulvey. &. Suppl. Rend. Circ. Mat. Palermo (2), 12:99-104, 1986. Google Scholar
  44. Christopher J Mulvey and Joan W Pelletier. A quantisation of the calculus of relations. In Canad. Math. Soc. Conf. Proc. 13, pages 345-360, 1992. Google Scholar
  45. Alan Mycroft, Dominic Orchard, and Tomas Petricek. Effect systems revisited—control-flow algebra and semantics. In Semantics, Logics, and Calculi, pages 1-32. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-27810-0_1.
  46. Flemming Nielson and Hanne Riis Nielson. From cml to process algebras. In International Conference on Concurrency Theory (CONCUR), pages 493-508. Springer, 1993. URL: http://dx.doi.org/10.1007/3-540-57208-2_34.
  47. Wesley Phoa. An introduction to fibrations, topos theory, the effective topos and modest sets. Technical Report ECS-LFCS-92-208, University of Edinburgh, 1992. Google Scholar
  48. Vaughan Pratt. Action logic and pure induction. In European Workshop on Logics in Artificial Intelligence, pages 97-120. Springer, 1990. URL: http://dx.doi.org/10.1007/BFb0018436.
  49. Lukas Rytz and Martin Odersky. Relative Effect Declarations for Lightweight Effect-Polymorphism. Technical Report EPFL-REPORT-175546, EPFL, 2012. Google Scholar
  50. Lukas Rytz, Martin Odersky, and Philipp Haller. Lightweight Polymorphic Effects. In European Conference on Object-Oriented Programming (ECOOP 2012), 2012. URL: http://dx.doi.org/10.1007/978-3-642-31057-7_13.
  51. Vijay A. Saraswat, Martin Rinard, and Prakash Panangaden. The Semantic Foundations of Concurrent Constraint Programming. In Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '91, pages 333-352. ACM, 1991. URL: http://dx.doi.org/10.1145/99583.99627.
  52. Christian Skalka. Types and trace effects for object orientation. Higher-Order and Symbolic Computation, 21(3):239-282, 2008. URL: http://dx.doi.org/10.1007/s10990-008-9032-6.
  53. Kohei Suenaga. Type-based deadlock-freedom verification for non-block-structured lock primitives and mutable references. In Asian Symposium on Programming Languages and Systems, pages 155-170. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-89330-1_12.
  54. Joshua Sunshine, Karl Naden, Sven Stork, Jonathan Aldrich, and Éric Tanter. First-class state change in plaid. In Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '11, pages 713-732, New York, NY, USA, 2011. ACM. URL: http://dx.doi.org/10.1145/2048066.2048122.
  55. Jean-Pierre Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of functional programming, 2(03):245-271, 1992. URL: http://dx.doi.org/10.1017/S0956796800000393.
  56. Ross Tate. The sequential semantics of producer effect systems. In POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages. ACM, 2013. URL: http://dx.doi.org/10.1145/2429069.2429074.
  57. Mads Tofte and Jean-Pierre 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, 1994. URL: http://dx.doi.org/10.1145/174675.177855.
  58. Matías Toro and Éric Tanter. Customizable gradual polymorphic effects for scala. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, pages 935-953. ACM, 2015. URL: http://dx.doi.org/10.1145/2814270.2814315.
  59. Marko van Dooren and Eric Steegmans. Combining the robustness of checked exceptions with the flexibility of unchecked exceptions using anchored exception declarations. In Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA '05, pages 455-471. ACM, 2005. URL: http://dx.doi.org/10.1145/1094811.1094847.
  60. Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. Gradual typestate. In ECOOP 2011 - Object-Oriented Programming - 25th European Conference, Lancaster, UK, July 25-29, 2011 Proceedings, pages 459-483, 2011. URL: http://dx.doi.org/10.1007/978-3-642-22655-7_22.
  61. David N Yetter. Quantales and (noncommutative) linear logic. The Journal of Symbolic Logic, 55(01):41-64, 1990. URL: http://dx.doi.org/10.2307/2274953.
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