Abstract
Implementing the type system of a programming language is a critical task that is often done in an ad-hoc fashion. Whilst this makes it hard to ensure the system is sound, it also makes it difficult to extend as the language evolves. We are interested in describing type systems using declarative rewrite rules from which an implementation can be automatically generated. Whilst not all type systems are easily expressed in this manner, those involving unions, intersections and negations are well-suited for this.
In this paper, we consider a relatively complex type system involving unions, intersections and negations developed previously. This system was not developed with rewriting in mind, though clear parallels are immediately apparent from the original presentation. For example, the system presented required types be first converted into a variation on Disjunctive Normal Form. We identify that the original system can, for the most part, be reworked to enable a natural expression using declarative rewrite rules. We present an implementation of our rewrite rules in the Whiley Rewrite Language (WyRL), and report performance results compared with a hand-coded solution.
- Ceylon Homepage. Retrieved 2017 from http://ceylon-lang.org/Google Scholar
- Facebook Flow. Retrieved 2017 from https://flowtype.org/Google Scholar
- Kotlin Homepage. Retrieved 2017 from http://kotlinlang.org/Google Scholar
- What's new in Groovy 2.0? Retrieved 2017 from http://www.infoq.com/articles/new-groovy-20Google Scholar
- Whiley Compiler Respository on GitHub. Retrieved 2017 from http://github.com/Whiley/WhileyCompilerGoogle Scholar
- The Whiley Programming Language. Retrieved 2017 from http://whiley.orgGoogle Scholar
- The Whiley Benchmark Suite. Retrieved 2017 from http://github.com/Whiley/WyBenchGoogle Scholar
- Alexander Aiken and Edward L. Wimmers. 1993. Type Inclusion Constraints and Type Inference. In Proceedings of the ACM conference on Functional Programming Languages and Computer Architecture (FPCA). 31-41. Google ScholarDigital Library
- Roberto M. Amadio and Luca Cardelli. 1993. Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15 (1993), 575-631. Issue 4. Google ScholarDigital Library
- Nada Amin and Ross Tate. 2016. Java and Scala's Type Systems Are Unsound: The Existential Crisis of Null Pointers. In Proceedings of the ACM conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). ACM Press, 838-848. Google ScholarDigital Library
- C. Andreae, J. Noble, S. Markstrum, and T. Millstein. 2006. A framework for implementing pluggable type systems. In Proceedings of the ACM conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). 57-74. Google ScholarDigital Library
- Véronique Benzaken, Giuseppe Castagna, and Alain Frisch. 2003. CDuce: An XML-Centric General-Purpose Language. In Proceedings of the ACM International Conference on Functional Programming (ICFP). 51-63. Google ScholarDigital Library
- Gavin M. Bierman, Martín Abadi, and Mads Torgersen. 2014. Understanding TypeScript. In Proceedings of the European Confereince on Object-Oriented Programming (ECOOP), Vol. 8586. Springer-Verlag, 257-281. Google ScholarDigital Library
- P. Borovansky, C. Kirchner, H. Kirchner, and P. Moreau. 2002. ELAN from a rewriting logic point of view. Theoretical Computer Science 285, 2 (2002), 155-185. Google ScholarDigital Library
- J. Bos, M. Hills, P. Klint, T. Storm, and J. Vinju. 2011. Rascal: From Algebraic Specification to Meta-Programming. In Proceedings Workshop on Algebraic Methods in Model-based Software Engineering, AMMSE (EPTCS), Vol. 56. 15-32.Google Scholar
- M. Brand, A. Deursen, P. Klint, S. Klusener, and E. Meulen. 1996. Industrial Applications of ASF+SDF. In Proceedings of the Conference on Algebraic Methodology and Software Technology (AMAST). 9-18. Google ScholarDigital Library
- M. Bravenboer, A. van Dam, K. Olmos, and E. Visser. 2006. Program Transformation with Scoped Dynamic Rewrite Rules. Fundamenta Informaticae 69, 1-2 (Winter 2006), 1-56. Google ScholarDigital Library
- Martin Büchi and Wolfgang Weck. 1998. Compound types for Java. In Proceedings of the ACM conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). 362-373. Google ScholarDigital Library
- Castagna and Frisch. 2005. A Gentle Introduction to Semantic Subtyping. In Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP). 198-199. Google ScholarDigital Library
- Philippe Charles, Robert M. Fuhrer, and Stanley M. Sutton Jr. 2007. IMP: a meta-tooling platform for creating language-specific ides in eclipse. In Proceedings of the Conference on Automated Software Engineering (ASE). ACM Press, 485-488. Google ScholarDigital Library
- M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada. 2002. Maude: specification and programming in rewriting logic. Theoretical Computer Science 285, 2 (2002), 187-243. Google ScholarDigital Library
- M. Clavel, F. Durán, S. Eker, P. Lincoln, J. Meseguer, and C. Talcott. 2003. The Maude 2.0 System. In Proceedings the Conference on Rewriting Techniques and Applications (RTA). 76-87. Google ScholarDigital Library
- James R. Cordy. 2006. The TXL source transformation language. Science of Computer Programming 61, 3 (2006), 190-210. Google ScholarDigital Library
- Flemming M. Damm. 1994. Subtyping with Union Types, Intersection Types and Recursive Types. In Proc. TACS. LNCS, Vol. 789. 687-706. Google ScholarDigital Library
- Ornela Dardha, Daniele Gorla, and Daniele Varacca. 2012. Semantic Subtyping for Objects and Classes. Technical Report. Laboratoire PPS, Université Paris Diderot.Google Scholar
- Razvan Diaconescu and Kokichi Futatsugi. 2002. Logical foundations of CafeOBJ. Theoretical Computer Science 285, 2 (2002), 289-318. Google ScholarDigital Library
- Charles Donnelly and Richard Stallman. 2000. Bison Manual: Using the YACC-compatible Parser Generator, for Version 1.29. Free Software Foundation, Inc.Google Scholar
- Torbjörn Ekman and Görel Hedin. 2005. Modular Name Analysis for Java Using JastAdd. In Proceedings of the Conference on Generative and Transformational Techniques in Software Engineering (GTTSE). Springer-Verlag, 422-436. Google ScholarDigital Library
- T. Ekman and G. Hedin. 2007. Pluggable Checking and Inferencing of Non-Null Types for Java. Journal of Object Technology 6, 9 (2007), 455-475.Google ScholarCross Ref
- Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva. 2015. ACoinductive Framework for Infinitary Rewriting and Equational Reasoning. In Proceedings the Conference on Rewriting Techniques and Applications (RTA). 143-159.Google Scholar
- Sebastian Erdweg, Tijs Van Der Storm, M. Voelter, M. Boersma, R. Bosman, William Cook, A. Gerritsen, A. Hulshout, S. Kelly, Alex Loh, G. Konat, P. J. Molina, M. Palatnik, R. Pohjonen, E. Schindler, K. Schindler, R. Solmi, V. Vergu, Van Der Vlist, K. B., G. Wachsmuth, Van Der Woning, and J. M. 2013. The State Of The Art In Language Workbenches. Conclusions From The Language Workbench Challenge. Springer-Verlag.Google Scholar
- Moritz Eysholdt and Heiko Behrens. 2010. Xtext: implement your language faster than the quick and dirty way. In SPLASH/OOPSLA Companion. ACM Press, 307-309. Google ScholarDigital Library
- M. Fähndrich and K. R. M. Leino. 2003. Declaring and checking nonnull types in an object-oriented language. In Proceedings of the ACM conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). ACM Press, 302-312. Google ScholarDigital Library
- A. Frisch, G. Castagna, and V. Benzaken. 2002. Semantic Subtyping. In Proceedings of the ACM/IEEE Symposium on Logic In Computer Science (LICS). IEEE Computer Society Press, 137-146. Google ScholarDigital Library
- A. Frisch, G. Castagna, and V. Benzaken. 2008. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM 55, 4 (2008), 19:1-19:64. Google ScholarDigital Library
- Andy Georges, Dries Buytaert, and Lieven Eeckhout. 2007. Statistically Rigorous Java Performance Evaluation. In Proceedings of the ACM conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). ACM Press, 57-76. Google ScholarDigital Library
- Sylvia Grewe, Sebastian Erdweg, and Mira Mezini. 2015. Using Vampire in Soundness Proofs of Type Systems. In Proceedings of Vampire Workshop. 33-51.Google Scholar
- Sylvia Grewe, Sebastian Erdweg, and Mira Mezini. 2016. Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny. In Proceedings of the Vampire Workshop, Vol. 44. 33-45.Google Scholar
- Sylvia Grewe, Sebastian Erdweg, Michael Raulf, and Mira Mezini. 2016. Exploration of language specifications by compilation to first-order logic. In Proceedings of the Symposium on Principles and Practice of Declarative Programming (PPDP). ACM Press, 104-117. Google ScholarDigital Library
- Sylvia Grewe, Sebastian Erdweg, Pascal Wittmann, and Mira Mezini. 2015. Type systems for the masses: deriving soundness proofs and efficient checkers. In Proceedings of the ACM conference Onward! ACM Press, 137-150. Google ScholarDigital Library
- Görel Hedin and Eva Magnusson. 2001. JastAdd - a Java-based system for implementing front ends. Electronic Notes in Computer Science 44, 2 (2001), 59-78.Google ScholarCross Ref
- J. Heering, P. R. H. Hendriks, P. Klint, and J. Rekers. 1989. The Syntax Definition Formalism SDF - reference manual -. ACM SIGPLAN Notices 24, 11 (1989), 43-75. Google ScholarDigital Library
- Mark Hills, Paul Klint, and Jurgen J. Vinju. 2012. Program Analysis Scenarios in Rascal. In Proceedings of the Workshop on Rewriting Logic and Its Applications (WRLA). Springer-Verlag, 10-30. Google ScholarDigital Library
- Haruo Hosoya and Benjamin C. Pierce. 2003. XDuce: A Statically Typed XML Processing Language. ACM Transactions on Internet Technology 3, 2 (2003), 117-148. Google ScholarDigital Library
- A. Igarashi and H. Nagira. 2006. Union types for object-oriented programming. In Proceedings of the Symposium on Applied Computing (SAC). 1435-1441. Google ScholarDigital Library
- JetBrains. Meta Programming System. Retrieved 2017 from http://www.jetbrains.com/mpsGoogle Scholar
- T. Jones and D. J. Pearce. 2016. A Mechanical Soundness Proof for Subtyping over Recursive Types. In Proceedings of the Workshop on Formal Techniques for Java-like Programs (FTFJP). article 1. Google ScholarDigital Library
- Lennart C. L. Kats and Eelco Visser. 2010. The Spoofax language workbench: Rules for declarative specification of languages and IDEs. In Proceedings of the ACM conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). ACM Press, 444-463. Google ScholarDigital Library
- Paul Klint, Tijs van der Storm, and Jurgen J. Vinju. 2009. RASCAL: A Domain Specific Language for Source Code Analysis and Manipulation. IEEE Computer Society Press, 168-177. Google ScholarDigital Library
- D. E. Knuth. 1981. The Art of Computer Programming, Volume 2: Seminumerical Algorithms. Second Edition, Addison-Wesley, Reading.Google Scholar
- Gabriël D. P. Konat, Lennart C. L. Kats, Guido Wachsmuth, and Eelco Visser. 2012. Declarative Name Binding and Scope Rules. In Proceedings of the Conference on Software Language Engineering (SLE). Springer-Verlag, 311-331.Google Scholar
- X. Leroy. 2003. Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning 30, 3/4 (2003), 235-269. Google ScholarDigital Library
- C. Male, D.J. Pearce, A. Potanin, and C. Dymnikov. 2008. Java Bytecode Verification for @NonNull Types. In Proceedings of the confererence on Compiler Construction (CC). 229-244. Google ScholarDigital Library
- Scott McPeak and George C. Necula. 2004. Elkhound: A Fast, Practical GLR Parser Generator. In Proceedings of the confererence on Compiler Construction (CC). Springer-Verlag, 73-88.Google Scholar
- José Meseguer. 2012. Twenty years of rewriting logic. Journal of Logic and Algebraic Programming 81, 7-8 (2012), 721-781.Google ScholarCross Ref
- Kazuhiro Ogata and Kokichi Futatsugi. 2004. Rewriting-Based Verification of Authentication Protocols. Electronic Notes in Computer Science 71 (2004), 208-222.Google ScholarCross Ref
- Terence Parr and Kathleen Fisher. 2011. LL(*): the foundation of the ANTLR parser generator. In Proceedings of the ACM conference on Programming Language Design and Implementation (PLDI). ACM Press, 425-436. Google ScholarDigital Library
- D. J. Pearce. 2013. A Calculus for Constraint-Based Flow Typing. In Proceedings of the Workshop on Formal Techniques for Java-like Programs (FTFJP). Article 7. Google ScholarDigital Library
- D. J. Pearce. 2013. Sound and Complete Flow Typing with Unions, Intersections and Negations. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). 335-354. Google ScholarDigital Library
- D. J. Pearce. 2015. Integer Range Analysis for Whiley on Embedded Systems. In Proceedings of the IEEE/IFIP Workshop on Software Technologies for Future Embedded and Ubiquitous Systems. 26-33. Google ScholarDigital Library
- D. J. Pearce. 2015. The Whiley Rewrite Language (WyRL). In Proceedings of the Conference on Software Language Engineering (SLE). 161-166. Google ScholarDigital Library
- D. J. Pearce. Updated, 2016. The Whiley Language Specification. (Updated, 2016).Google Scholar
- D. J. Pearce and L. Groves. 2013. Whiley: a Platform for Research in Software Verification. In Proceedings of the Conference on Software Language Engineering (SLE). 238-248.Google Scholar
- D. J. Pearce and L. Groves. 2015. Designing a Verifying Compiler: Lessons Learned from Developing Whiley. Science of Computer Programming (2015), 191-220. Google ScholarDigital Library
- Martin Plümicke. 2008. Intersection types in Java. In Proceedings of the conference on Principles and Practices of Programming in Java (PPPJ). ACM Press, 181-188. Google ScholarDigital Library
- Michael Roberson, Melanie Harries, Paul T. Darga, and Chandrasekhar Boyapati. 2008. Efficient software model checking of soundness of type systems. In Proceedings of the ACM conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). ACM Press, 493-504. Google ScholarDigital Library
- Sebastian Schweizer. 2016. Lifetime Analysis for Whiley. Master's Thesis. Department of Computer Science, University of Kaiserslautern.Google Scholar
- Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The design and implementation of Typed Scheme. In Proceedings of the ACM symposium on the Principles Of Programming Languages (POPL). 395-406. Google ScholarDigital Library
- S. Tobin-Hochstadt and M. Felleisen. 2010. Logical types for untyped languages. In Proceedings of the ACM International Conference on Functional Programming (ICFP). 117-128. Google ScholarDigital Library
- Mark van den Brand, Arie van Deursen, Jan Heering, H. A. de Jong, Merijn de Jonge, Tobias Kuipers, Paul Klint, Leon Moonen, Pieter A. Olivier, Jeroen Scheerder, Jurgen J. Vinju, Eelco Visser, and Joost Visser. 2001. The ASF+SDF Meta-environment: A Component-Based Language Development Environment. In Proceedings of the confererence on Compiler Construction (CC) (LNCS), Vol. 2027. Springer-Verlag, 365-370. Google ScholarDigital Library
- Arie van Deursen, Jan Heering, and Paul Klint (Eds.). 1996. Language Prototyping: An Algebraic Specification Approach. Google ScholarDigital Library
- Eelco Visser. 2001. Stratego: A Language for Program Transformation Based on Rewriting Strategies. In Proceedings the Conference on Rewriting Techniques and Applications (RTA). 357-362. Google ScholarDigital Library
- Eelco Visser, Guido Wachsmuth, Andrew P. Tolmach, Pierre Neron, Vlad A. Vergu, Augusto Passalaqua, and Gabrieël Konat. 2014. A Language Designer's Workbench: A One-Stop-Shop for Implementation and Verification of Language Designs. In Proceedings of the ACM conference Onward! ACM Press, 95-111. Google ScholarDigital Library
- Markus Voelter and Vaclav Pech. 2012. Language modularity with the MPS language workbench. In Proceedings of the International Conference of Software Engineering (ICSE). IEEE Computer Society Press, 1449-1450. Google ScholarDigital Library
- Guido Wachsmuth, Gabriël D. P. Konat, and Eelco Visser. 2014. Language Design with the Spoofax Language Workbench. IEEE Software 31, 5 (2014), 35-43.Google ScholarCross Ref
Index Terms
Rewriting for sound and complete union, intersection and negation types
Recommendations
Rewriting for sound and complete union, intersection and negation types
GPCE 2017: Proceedings of the 16th ACM SIGPLAN International Conference on Generative Programming: Concepts and ExperiencesImplementing the type system of a programming language is a critical task that is often done in an ad-hoc fashion. Whilst this makes it hard to ensure the system is sound, it also makes it difficult to extend as the language evolves. We are interested ...
Elaborating intersection and union types
ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programmingDesigning and implementing typed programming languages is hard. Every new type system feature requires extending the metatheory and implementation, which are often complicated and fragile. To ease this process, we would like to provide general ...
Elaborating intersection and union types
ICFP '12Designing and implementing typed programming languages is hard. Every new type system feature requires extending the metatheory and implementation, which are often complicated and fragile. To ease this process, we would like to provide general ...
Comments