Hostname: page-component-745bb68f8f-5r2nc Total loading time: 0 Render date: 2025-01-07T15:12:17.501Z Has data issue: false hasContentIssue false
  • English
  • Français

Gradual type-and-effect systems

Part of: JFP Research Articles

Published online by Cambridge University Press:  22 September 2016

FELIPE BAÑADOS SCHWERTER ,
RONALD GARCIA  and
ÉRIC TANTER
FELIPE BAÑADOS SCHWERTER
Affiliation:
Software Practices Lab, Department of Computer Science, University of British Columbia, Vancouver, BC, Canada (e-mails: fbanados@cs.ubc.ca, rxg@cs.ubc.ca)
RONALD GARCIA
Affiliation:
Software Practices Lab, Department of Computer Science, University of British Columbia, Vancouver, BC, Canada (e-mails: fbanados@cs.ubc.ca, rxg@cs.ubc.ca)
ÉRIC TANTER
Affiliation:
PLEIAD Lab, Computer Science Department (DCC), University of Chile, Santiago, Chile (e-mail: etanter@dcc.uchile.cl)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Effect systems have the potential to help software developers, but their practical adoption has been very limited. We conjecture that this limited adoption is due in part to the difficulty of transitioning from a system where effects are implicit and unrestricted to a system with a static effect discipline, which must settle for conservative checking in order to be decidable. To address this hindrance, we develop a theory of gradual effect checking, which makes it possible to incrementally annotate and statically check effects, while still rejecting statically inconsistent programs. We extend the generic type-and-effect framework of Marino and Millstein with a notion of unknown effects, which turns out to be significantly more subtle than unknown types in traditional gradual typing. We appeal to abstract interpretation to develop and validate the concepts of gradual effect checking. We also demonstrate how an effect system formulated in the framework of Marino and Millstein can be automatically extended to support gradual checking. We use gradual effect checking to develop a fully gradual type-and-effect framework, which permits interaction between static and dynamic checking for both effects and types.

Type
Articles
Information
Journal of Functional Programming , Volume 26 , 2016 , e19
Copyright
Copyright © Cambridge University Press 2016 

References

Abadi, M., Birrell, A., Harris, T. & Isard, M. (2008) Semantics of transactional memory and automatic mutual exclusion. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008). New York, NY, USA: ACM Press, pp. 63–74.CrossRefGoogle Scholar
Abadi, M., Flanagan, C. & Freund, S. N. (2006) Types for safe locking: Static race detection for java. ACM Trans. Program. Lang. Syst. 28 (2), 207–255.CrossRefGoogle Scholar
Bañados Schwerter, F., Garcia, R. & Tanter, É. (2014) A theory of gradual effect systems. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP 2014). New York, NY, USA: ACM Press, pp. 283–295.CrossRefGoogle Scholar
Benton, N. & Buchlovsky, P. (2007) Semantics of an effect analysis for exceptions. In Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI 2007). New York, NY, USA: ACM Press, pp. 15–26.CrossRefGoogle Scholar
Cousot, P. & Cousot, R. (1977) Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL 1977). New York, NY, USA: ACM Press, pp. 238–252.CrossRefGoogle Scholar
Cousot, P. & Cousot, R. (1979) Systematic design of program analysis frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 1979). New York, NY, USA: ACM Press, pp. 269–282.CrossRefGoogle Scholar
Delaware, B., Keuchel, S., Schrijvers, T. & Oliveira, B. C.d.S. (2013) Modular monadic meta-theory. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP 2013). New York, NY, USA: ACM Press, pp. 319–330.CrossRefGoogle Scholar
Disney, T. & Flanagan, C. (2011) Gradual information flow typing. In International Workshop on Scripts to Programs (STOP 2011), Co-Located with POPL 2011. Url: https://users.soe.ucsc.edu/~cormac/papers/stop11.pdf.Google Scholar
Disney, T., Flanagan, C. & McCarthy, J. (2011) Temporal higher-order contracts. In Proceedings of the 16th ACM SIGPLAN Conference on Functional Programming (ICFP 2011). New York, NY, USA: ACM Press, pp. 176–188.CrossRefGoogle Scholar
Fennell, L. & Thiemann, P. (2013 June) Gradual security typing with references. In Computer Security Foundations Symposium (csf), Los Alamitos, CA, USA: IEEE, pp. 224–239.CrossRefGoogle Scholar
Findler, R. B. & Felleisen, M. (2002) Contracts for higher-order functions. In Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming (ICFP 2002). New York, NY, USA: ACM Press, pp. 48–59.CrossRefGoogle Scholar
Garcia, R., Clark, A. M. & Tanter, É. (2016) Abstracting gradual typing. In Proceedings of the 43rd Annual ACM Sigplan-Sigact Symposium on Principles of Programming Languages (POPL 2016). New York, NY, USA: ACM Press, pp. 429–442.CrossRefGoogle Scholar
Garcia, R., Tanter, É., Wolff, R. & Aldrich, J. (2014) Foundations of typestate-oriented programming. ACM Trans. Program. Lang. Syst. 36 (4), 12:1–12:44.CrossRefGoogle Scholar
Gifford, D. K. & Lucassen, J. M. (1986) Integrating functional and imperative programming. In Proceedings of the 1986 ACM Conference on Lisp and Functional Programming. New York, NY, USA: ACM Press, pp. 28–38.CrossRefGoogle Scholar
Gordon, C. S., Dietl, W., Ernst, M. D. & Grossman, D. (2013) JavaUI: Effects for controlling UI object access. In Proceedings of the 27th European Conference on Object-oriented Programming (ECOOP 2013). Berlin, Germany: Springer-Verlag, pp. 179–204.Google Scholar
Gosling, J., Joy, B., Steele, G. & Bracha, G. (2003) The Java Language Specification, 3rd ed. Addison-Wesley.Google Scholar
Ina, L. & Igarashi, A. (2011) Gradual typing for generics. In Proceedings of the 26th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2011). New York, NY, USA: ACM Press, pp. 609–624.CrossRefGoogle Scholar
Marino, D. & Millstein, T. (2009) A generic type-and-effect system. In Proceedings of the ACM SIGPLAN International Workshop on Types in Language Design and Implementation, New York, NY, USA: ACM Press, pp. 39–50.CrossRefGoogle Scholar
Pierce, B. C. (2002) Types and Programming Languages. MIT Press.Google Scholar
Rytz, L., Amin, N. & Odersky, M. (2013) A flow-insensitive, modular effect system for purity. In Proceedings of the 15th Workshop on Formal Techniques for Java-like Programs. New York, NY, USA: ACM Press, pp. 4:1–4:7.CrossRefGoogle Scholar
Rytz, L., Odersky, M. & Haller, P. (2012) Lightweight polymorphic effects. In Proceedings of the 26th European Conference on Object-oriented Programming (ECOOP 2012). Berlin, Germany: Springer-Verlag, pp. 258–282.CrossRefGoogle Scholar
Scholliers, C., Tanter, É. & De Meuter, W. (2015) Computational contracts. Sci. Comput. Program. 98 (3), 360–375.CrossRefGoogle Scholar
Sergey, I. & Clarke, D. (2012) Gradual ownership types. In Proceedings of the 21st European Symposium on Programming Languages and Systems (ESOP 2012). Berlin, Germany: Springer-Verlag, pp. 579–599.CrossRefGoogle Scholar
Siek, J. & Taha, W. (2007) Gradual typing for objects. In Proceedings of the 21st European Conference on Object-oriented Programming (ECOOP 2007). Berlin, Germany: Springer-Verlag, pp. 2–27.CrossRefGoogle Scholar
Siek, J. G. & Taha, W. (2006 September) Gradual typing for functional languages. In Proceedings of the Scheme and Functional Programming Workshop, Chicago, IL, USA: University of Chicago TR-2006-06, pp. 81–92.Google Scholar
Takikawa, A., Strickland, T. S., Dimoulas, C., Tobin-Hochstadt, S. & Felleisen, M. (2012) Gradual typing for first-class classes. In Proceedings of the 27th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2012). New York, NY, USA: ACM Press, pp. 793–810.CrossRefGoogle Scholar
Tang, Y. M. & Jouvelot, P. (1995) Effect systems with subtyping. In Proceedings of the 1995 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation (PEPM 1995). New York, NY, USA: ACM Press, pp. 45–53.CrossRefGoogle Scholar
Thiemann, P. & Fennell, L. (2014) Gradual typing for annotated type systems. In Programming Languages and Systems. Lecture Notes in Computer Science, vol. 8410. Springer, Berlin Heidelberg.Google Scholar
Toro, M. & Tanter, É. (2015) Customizable gradual polymorphic effects for scala. In Submission to the 30th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2015), New York, NY, USA: ACM Press.CrossRefGoogle Scholar
Wolff, R., Garcia, R., Tanter, É. & Aldrich, J. (2011) Gradual typestate. In Proceedings of the 25th European Conference on Object-oriented Programming (ECOOP 2011). Berlin, Germany: Springer-Verlag, pp. 459–483.CrossRefGoogle Scholar
Wright, A. K. & Felleisen, M. (1994) A syntactic approach to type soundness. J. Inform. Comput. 115 (1), 38–94.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.