Document Open Access Logo

Intensional Effect Polymorphism

Authors Yuheng Long, Yu David Liu, Hridesh Rajan

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2015.346.pdf
  • Filesize: 0.68 MB
  • 25 pages

Document Identifiers

Author Details

Yuheng Long
Yu David Liu
Hridesh Rajan

Cite As Get BibTex

Yuheng Long, Yu David Liu, and Hridesh Rajan. Intensional Effect Polymorphism. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 346-370, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.ECOOP.2015.346

Abstract

Type-and-effect systems are a powerful tool for program construction and verification. We describe intensional effect polymorphism, a new foundation for effect systems that integrates static and dynamic effect checking. Our system allows the effect of polymorphic code to be intensionally inspected through a lightweight notion of dynamic typing. When coupled with parametric polymorphism, the powerful system utilizes runtime information to enable precise effect reasoning, while at the same time retains strong type safety guarantees. We build our ideas on top of an imperative core calculus with regions. The technical innovations of our design include a relational notion of effect checking, the use of bounded existential types to capture the subtle interactions between static typing and dynamic typing, and a differential alignment strategy to achieve efficiency in dynamic typing. We demonstrate the applications of intensional effect polymorphism in concurrent programming, security, graphical user interface access, and memoization.

Subject Classification

Keywords
  • intensional effect polymorphism
  • type system
  • hybrid typing

Metrics

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

References

  1. M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic typing in a statically-typed language. In Proceedings of the Symposium on Principles of Programming Languages, 1989. Google Scholar
  2. 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, 2006. Google Scholar
  3. Ole Agesen. Concrete type inference: delivering object-oriented applications. PhD thesis, Stanford University, Stanford, CA, USA, 1996. Google Scholar
  4. Alexander Aiken, Edward L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages, 1994. Google Scholar
  5. Felipe Bañados, Ronald Garcia, and Éric Tanter. A theory of gradual effect systems. In Proceedings of the 19th ACM SIGPLAN Conference on Functional Programming, 2014. Google Scholar
  6. Nick Benton and Peter Buchlovsky. Semantics of an effect analysis for exceptions. In Proceedings of the international workshop on Types in languages design and implementation, 2007. Google Scholar
  7. Guy E. Blelloch. Prefix sums and their applications. Google Scholar
  8. Robert L. Bocchino and Vikram S. Adve. Types, regions, and effects for safe programming with object-oriented parallel frameworks. In Proceedings of the 25th European Conference on Object-oriented Programming, 2011. Google Scholar
  9. Sebastian Burckhardt, Daan Leijen, Caitlin Sadowski, Jaeheon Yi, and Thomas Ball. Two for the price of one: A model for parallel and incremental computation. In Proceedings of the International Conference on Object Oriented Programming Systems Languages and Applications, 2011. Google Scholar
  10. Robert Cartwright and Mike Fagan. Soft typing. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 1991. Google Scholar
  11. Ravi Chugh, Jeffrey A. Meister, Ranjit Jhala, and Sorin Lerner. Staged information flow for JavaScript. In Proceedings of Conference on Programming Language Design and Implementation, 2009. Google Scholar
  12. Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type-erasure semantics. In Proceedings of the International Conference on Functional Programming, 1998. Google Scholar
  13. Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1982. Google Scholar
  14. Cormac Flanagan. Hybrid type checking. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006. Google Scholar
  15. Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. Flow-sensitive type qualifiers. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2002. Google Scholar
  16. Colin S. Gordon, Werner Dietl, Michael D. Ernst, and Dan Grossman. JavaUI: Effects for controlling UI object access. In the European Conference on Object-Oriented Programming, 2013. Google Scholar
  17. Aaron Greenhouse and John Boyland. An object-oriented effects system. In Proceedings of the 13th European Conference on Object-Oriented Programming, 1999. Google Scholar
  18. Brian Hackett and Shu-yu Guo. Fast and precise hybrid type inference for JavaScript. In Proceedings of the Conference on Programming Language Design and Implementation, 2012. Google Scholar
  19. Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. In Proceedings of the Symposium on Principles of Programming Languages, 1995. Google Scholar
  20. Stephen T. Heumann, Vikram S. Adve, and Shengjie Wang. The tasks with effects model for safe concurrency. In Proceedings of the Symposium on Principles and Practice of Parallel Programming, 2013. Google Scholar
  21. Aditya Kulkarni, Yu David Liu, and Scott F. Smith. Task types for pervasive atomicity. In the conference on Object-oriented programming, systems, languages, and applications, 2010. Google Scholar
  22. B. W. Lampson, J. J. Horning, R. L. London, J. G. Mitchell, and G. J. Popek. Report on the programming language Euclid. SIGPLAN Not., 12(2):1-79, 1977. Google Scholar
  23. Anatole Le, Ondřej Lhoták, and Laurie Hendren. Using inter-procedural side-effect information in JIT optimizations. In the International Conference on Compiler Construction, 2005. Google Scholar
  24. Xavier Leroy and François Pessaux. Type-based analysis of uncaught exceptions. ACM Trans. Program. Lang. Syst., 22(2), 2000. Google Scholar
  25. Yuheng Long, Yu David Liu, and Hridesh Rajan. Hybrid Effect Checking. Technical report, Iowa State University, 2014. Google Scholar
  26. Yuheng Long, Sean L. Mooney, Tyler Sondag, and Hridesh Rajan. Implicit invocation meets safe, implicit concurrency. In Ninth International Conference on Generative Programming and Component Engineering, 2010. Google Scholar
  27. J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1988. Google Scholar
  28. Daniel Marino and Todd Millstein. A generic type-and-effect system. In Proceedings of the 4th international workshop on Types in language design and implementation, 2009. Google Scholar
  29. Iulian Neamtiu, Michael Hicks, Jeffrey S. Foster, and Polyvios Pratikakis. Contextual effects for version-consistent dynamic software updating and safe concurrent programming. In Proceedings of the ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 2008. Google Scholar
  30. Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. Google Scholar
  31. Andreas Rossberg. Dynamic translucency with abstraction kinds and higher-order coercions. Electron. Notes Theor. Comput. Sci., 218:313-336, 2008. Google Scholar
  32. Lukas Rytz, Martin Odersky, and Philipp Haller. Lightweight polymorphic effects. In Proceedings of the 26th European Conference on Object-Oriented Programming, 2012. Google Scholar
  33. Olin Grigsby Shivers. Control-flow Analysis of Higher-order Languages or Taming Lambda. PhD thesis, Carnegie Mellon University, 1991. Google Scholar
  34. Jeremy Siek and Walid Taha. Gradual typing for objects. In Proceedings of the 21st European Conference on Object-Oriented Programming, 2007. Google Scholar
  35. R E Strom and S Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng., 12(1), 1986. Google Scholar
  36. Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Inf. Comput., 111(2), 1994. Google Scholar
  37. Mads Tofte. Type inference for polymorphic references. Inf. Comput., 89(1), 1990. Google Scholar
  38. Sean Treichler, Michael Bauer, and Alex Aiken. Language support for dynamic, hierarchical data partitioning. In Proceedings of the ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages and Applications, 2013. 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 About DROPS Imprint Privacy Contact