First-class effect reflection for effect-guided programming
Abstract
This paper introduces a novel type-and-effect calculus, first-class effects, where the computational effect of an expression can be programmatically reflected, passed around as values, and analyzed at run time. A broad range of designs "hard-coded" in existing effect-guided analyses — from thread scheduling, version-consistent software updating, to data zeroing — can be naturally supported through the programming abstractions. The core technical development is a type system with a number of features, including a hybrid type system that integrates static and dynamic effect analyses, a refinement type system to verify application-specific effect management properties, a double-bounded type system that computes both over-approximation of effects and their under-approximation. We introduce and establish a notion of soundness called trace consistency, defined in terms of how the effect and trace correspond. The property sheds foundational insight on "good" first-class effect programming.
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.
[2]
F. Bañados Schwerter, R. Garcia, and E. Tanter. A theory of gradual effect systems. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2014.
[3]
M. Bagherzadeh and H. Rajan. Panini: A concurrent programming model for solving pervasive and oblivious interference. In the International Conference on Modularity, 2015.
[4]
A. Bauer and M. Pretnar. Programming with algebraic effects and handlers. CoRR, 2012.
[5]
E. Bertino, S. Jajodia, and P. Samarati. Supporting multiple access control policies in database systems. In Proceedings of the IEEE Symposium on Security and Privacy, 1996.
[6]
R. L. Bocchino and V. S. Adve. Types, regions, and effects for safe programming with object-oriented parallel frameworks. In Proceedings of the 25th European Conference on Objectoriented Programming, 2011.
[7]
P. Boström and P. Müller. Modular verification of finite blocking in non-terminating programs. In Proceedings of the European Conference on Object-oriented Programming, 2015.
[8]
S. Burckhardt, A. Baldassin, and D. Leijen. Concurrent programming with revisions and isolation types. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, 2010.
[9]
S. Burckhardt, P. Kothari, M. Musuvathi, and S. Nagarakatte. A randomized scheduler with probabilistic guarantees of finding bugs. In Proceedings of the Fifteenth Edition of ASPLOS on Architectural Support for Programming Languages and Operating Systems, 2010.
[10]
J. Burnim, T. Elmas, G. Necula, and K. Sen. Concurrit: Testing concurrent programs with programmable state-space exploration. In Proceedings of the 4th USENIX Conference on Hot Topics in Parallelism, 2012.
[11]
R. Chugh, J. A. Meister, R. Jhala, and S. Lerner. Staged information flow for JavaScript. In the Conference on Programming Language Design and Implementation, 2009.
[12]
R. Chugh, D. Herman, and R. Jhala. Dependent types for JavaScript. In the Conference on Object Oriented Programming Systems Languages and Applications, 2012.
[13]
R. Chugh, P. M. Rondon, and R. Jhala. Nested refinements: A logic for duck typing. In the Symposium on Principles of Programming Languages, 2012.
[14]
D. Clarke and S. Drossopoulou. Ownership, encapsulation and the disjointness of type and effect. In Proceedings of the 17th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, 2002.
[15]
F. Craciun, W.-N. Chin, G. He, and S. Qin. An intervalbased inference of variant parametric types. In the European Symposium on Programming Languages and Systems, 2009.
[16]
K. Crary, S. Weirich, and G. Morrisett. Intensional polymorphism in type-erasure semantics. In Proceedings of the International Conference on Functional Programming, 1998.
[17]
J. Dean and S. Ghemawat. Mapreduce: Simplified data processing on large clusters. In the Conference on Symposium on Opearting Systems Design & Implementation, 2004.
[18]
R. Dyer. Task fusion: Improving utilization of multi-user clusters. In Proceedings of the 2013 Companion Publication for Conference on Systems, Programming, and Applications: Software for Humanity, 2013.
[19]
J. Erickson, M. Musuvathi, S. Burckhardt, and K. Olynyk. Effective data-race detection for the kernel. In Proceedings of the 9th USENIX Conference on Operating Systems Design and Implementation, 2010.
[20]
M. D. Ernst, C. S. Kaplan, and C. Chambers. Predicate dispatching: A unified theory of dispatch. In the European Conference on Object-Oriented Programming, 1998.
[21]
J. S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. In Proceedings of the Conference on Programming Language Design and Implementation, 2002.
[22]
T. Freeman and F. Pfenning. Refinement types for ML. In Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation, 1991.
[23]
A. Gotsman, B. Cook, M. Parkinson, and V. Vafeiadis. Proving that non-blocking algorithms don’t block. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009.
[24]
A. Greenhouse and J. Boyland. An object-oriented effects system. In Proceedings of the 13th European Conference on Object-Oriented Programming. 1999.
[25]
A. Guha, C. Saftoiu, and S. Krishnamurthi. Typing local control and state using flow analysis. In the European Conference on Programming Languages and Systems, 2011.
[26]
R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Proceedings of the Symposium on Principles of Programming Languages, 1995.
[27]
S. T. Heumann, V. S. Adve, and S. Wang. The tasks with effects model for safe concurrency. In Proceedings of the 18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2013.
[28]
A. Kulkarni, Y. D. Liu, and S. F. Smith. Task types for pervasive atomicity. In the conference on Object-oriented programming, systems, languages, and applications, 2010.
[29]
M. Kulkarni, P. Carribault, K. Pingali, G. Ramanarayanan, B. Walter, K. Bala, and L. P. Chew. Scheduling strategies for optimistic parallel execution of irregular programs. In Proceedings of the Twentieth Annual Symposium on Parallelism in Algorithms and Architectures, 2008.
[30]
A. Le, O. Lhoták, and L. Hendren. Using inter-procedural side-effect information in JIT optimizations. In the International Conference on Compiler Construction, 2005.
[31]
D. Lea. A Java fork/join framework. In Proceedings of the ACM 2000 Conference on Java Grande, 2000.
[32]
X. Leroy and F. Pessaux. Type-based analysis of uncaught exceptions. ACM Trans. Program. Lang. Syst., 22, 2000.
[33]
Y. Long and H. Rajan. First-Class Effect Reflection for Effect-Guided Programming. Technical Report 16-1, Iowa State U., Computer Sc., 2016.
[34]
Y. Long and H. Rajan. A type-and-effect system for asynchronous, typed events. In Proceedings of the 15th International Conference on Modularity, 2016.
[35]
Y. Long, Y. D. Liu, and H. Rajan. Intensional effect polymorphism. In Proceedings of the 29th European Conference on Object-oriented Programming, 2015.
[36]
S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: A comprehensive study on real world concurrency bug characteristics. In Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems, 2008.
[37]
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.
[38]
D. Marino and T. Millstein. A generic type-and-effect system. In Proceedings of the 4th international workshop on Types in language design and implementation, 2009.
[39]
T. Millstein. Practical predicate dispatch. In Proceedings of the ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, 2004.
[40]
S. Narayanasamy, Z. Wang, J. Tigani, A. Edwards, and B. Calder. Automatically classifying benign and harmful data races using replay analysis. In the Conference on Programming Language Design and Implementation, 2007.
[41]
I. Neamtiu, M. Hicks, G. Stoyle, and M. Oriol. Practical dynamic software updating for C. In PLDI ’06.
[42]
I. Neamtiu, M. Hicks, J. S. Foster, and P. Pratikakis. Contextual effects for version-consistent dynamic software updating and safe concurrent programming. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 2008.
[43]
F. Nielson and H. R. Nielson. Type and effect systems. In Correct System Design, 1999.
[44]
N. Nystrom, V. Saraswat, J. Palsberg, and C. Grothoff. Constrained types for object-oriented languages. In Proceedings of the 23rd ACM SIGPLAN Conference on Object-oriented Programming Systems Languages and Applications, 2008.
[45]
J. Philbin, J. Edler, O. J. Anshus, C. C. Douglas, and K. Li. Thread scheduling for cache locality. In Proceedings of the Seventh International Conference on Architectural Support for Programming Languages and Operating Systems, 1996.
[46]
K. Pingali, D. Nguyen, M. Kulkarni, M. Burtscher, M. A. Hassaan, R. Kaleem, T.-H. Lee, A. Lenharth, R. Manevich, M. Méndez-Lojo, D. Prountzos, and X. Sui. The tao of parallelism in algorithms. In the Conference on Programming Language Design and Implementation, 2011.
[47]
H. Rajan and G. T. Leavens. Ptolemy: A language with quantified, typed events. In ECOOP ’08.
[48]
K. Ravichandran and S. Pande. Multiverse: Efficiently supporting distributed high-level speculation. In Proceedings of the International Conference on Object Oriented Programming Systems Languages and Applications, 2013.
[49]
F. B. Schneider. Enforceable security policies. ACM Trans. Inf. Syst. Secur., 3, 2000.
[50]
J. Siek and W. Taha. Gradual typing for objects. In Proceedings of the 21st European Conference on Object-Oriented Programming, 2007.
[51]
D. Smith and R. Cartwright. Java type inference is broken: Can we fix it? In Proceedings of the 23rd ACM SIGPLAN Conference on Object-oriented Programming Systems Languages and Applications, 2008.
[52]
J.-P. Talpin and P. Jouvelot. The type and effect discipline. Inf. Comput., 111, 1994.
[53]
M. Toro and É. Tanter. Customizable gradual polymorphic effects for Scala. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2015.
[54]
S. Treichler, M. Bauer, and A. 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.
[55]
X. Yang, S. M. Blackburn, D. Frampton, J. B. Sartor, and K. S. McKinley. Why nothing matters: The impact of zeroing. In the Conference on Object Oriented Programming Systems Languages and Applications, 2011.
[56]
J. Yi and C. Flanagan. Effects for cooperable and serializable threads. In Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, 2010.
Index Terms
- First-class effect reflection for effect-guided programming
Recommendations
First-class effect reflection for effect-guided programming
OOPSLA 2016: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and ApplicationsThis paper introduces a novel type-and-effect calculus, first-class effects, where the computational effect of an expression can be programmatically reflected, passed around as values, and analyzed at run time. A broad range of designs "hard-coded" in ...
Typeless programming in Java 5.0 with wildcards
PPPJ '07: Proceedings of the 5th international symposium on Principles and practice of programming in JavaWith the introduction of Java 5.0 [8] the type system has been extended by parameterized types, type variables, type terms, and wildcards. As a result very complex types can arise. The term Vector<? super Vector<? extends List<Integer>>> is for example ...
Typeless programming in Java 5.0
PPPJ '06: Proceedings of the 4th international symposium on Principles and practice of programming in JavaWith the introduction of Java 5.0 [9] the type system has been extended by parameterized types, type variables, type terms, and wildcards. As a result very complex types can arise. The termVector<Vector<AbstractList<Integer>>>is for example a correct ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2016
915 pages
October 2016915 pages
Copyright © 2016 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]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 19 October 2016
Published in SIGPLAN Volume 51, Issue 10
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 164Total Downloads
- Downloads (Last 12 months)4
- Downloads (Last 6 weeks)0
Reflects downloads up to 13 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in