skip to main content
article

Rewriting for sound and complete union, intersection and negation types

Published:23 October 2017Publication History
Skip Abstract Section

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.

References

  1. Ceylon Homepage. Retrieved 2017 from http://ceylon-lang.org/Google ScholarGoogle Scholar
  2. Facebook Flow. Retrieved 2017 from https://flowtype.org/Google ScholarGoogle Scholar
  3. Kotlin Homepage. Retrieved 2017 from http://kotlinlang.org/Google ScholarGoogle Scholar
  4. What's new in Groovy 2.0? Retrieved 2017 from http://www.infoq.com/articles/new-groovy-20Google ScholarGoogle Scholar
  5. Whiley Compiler Respository on GitHub. Retrieved 2017 from http://github.com/Whiley/WhileyCompilerGoogle ScholarGoogle Scholar
  6. The Whiley Programming Language. Retrieved 2017 from http://whiley.orgGoogle ScholarGoogle Scholar
  7. The Whiley Benchmark Suite. Retrieved 2017 from http://github.com/Whiley/WyBenchGoogle ScholarGoogle Scholar
  8. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  9. Roberto M. Amadio and Luca Cardelli. 1993. Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15 (1993), 575-631. Issue 4. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  11. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  12. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  13. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  14. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  15. 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 ScholarGoogle Scholar
  16. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  17. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  18. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  19. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  20. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  21. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  22. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  23. James R. Cordy. 2006. The TXL source transformation language. Science of Computer Programming 61, 3 (2006), 190-210. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. Flemming M. Damm. 1994. Subtyping with Union Types, Intersection Types and Recursive Types. In Proc. TACS. LNCS, Vol. 789. 687-706. Google ScholarGoogle ScholarDigital LibraryDigital Library
  25. Ornela Dardha, Daniele Gorla, and Daniele Varacca. 2012. Semantic Subtyping for Objects and Classes. Technical Report. Laboratoire PPS, Université Paris Diderot.Google ScholarGoogle Scholar
  26. Razvan Diaconescu and Kokichi Futatsugi. 2002. Logical foundations of CafeOBJ. Theoretical Computer Science 285, 2 (2002), 289-318. Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. Charles Donnelly and Richard Stallman. 2000. Bison Manual: Using the YACC-compatible Parser Generator, for Version 1.29. Free Software Foundation, Inc.Google ScholarGoogle Scholar
  28. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  29. 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 ScholarGoogle ScholarCross RefCross Ref
  30. 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 ScholarGoogle Scholar
  31. 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 ScholarGoogle Scholar
  32. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  33. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  34. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  35. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  36. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  37. Sylvia Grewe, Sebastian Erdweg, and Mira Mezini. 2015. Using Vampire in Soundness Proofs of Type Systems. In Proceedings of Vampire Workshop. 33-51.Google ScholarGoogle Scholar
  38. 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 ScholarGoogle Scholar
  39. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  40. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  41. 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 ScholarGoogle ScholarCross RefCross Ref
  42. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  43. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  44. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  45. A. Igarashi and H. Nagira. 2006. Union types for object-oriented programming. In Proceedings of the Symposium on Applied Computing (SAC). 1435-1441. Google ScholarGoogle ScholarDigital LibraryDigital Library
  46. JetBrains. Meta Programming System. Retrieved 2017 from http://www.jetbrains.com/mpsGoogle ScholarGoogle Scholar
  47. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  48. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  49. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  50. D. E. Knuth. 1981. The Art of Computer Programming, Volume 2: Seminumerical Algorithms. Second Edition, Addison-Wesley, Reading.Google ScholarGoogle Scholar
  51. 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 ScholarGoogle Scholar
  52. X. Leroy. 2003. Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning 30, 3/4 (2003), 235-269. Google ScholarGoogle ScholarDigital LibraryDigital Library
  53. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  54. 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 ScholarGoogle Scholar
  55. José Meseguer. 2012. Twenty years of rewriting logic. Journal of Logic and Algebraic Programming 81, 7-8 (2012), 721-781.Google ScholarGoogle ScholarCross RefCross Ref
  56. Kazuhiro Ogata and Kokichi Futatsugi. 2004. Rewriting-Based Verification of Authentication Protocols. Electronic Notes in Computer Science 71 (2004), 208-222.Google ScholarGoogle ScholarCross RefCross Ref
  57. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  58. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  59. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  60. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  61. D. J. Pearce. 2015. The Whiley Rewrite Language (WyRL). In Proceedings of the Conference on Software Language Engineering (SLE). 161-166. Google ScholarGoogle ScholarDigital LibraryDigital Library
  62. D. J. Pearce. Updated, 2016. The Whiley Language Specification. (Updated, 2016).Google ScholarGoogle Scholar
  63. 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 ScholarGoogle Scholar
  64. D. J. Pearce and L. Groves. 2015. Designing a Verifying Compiler: Lessons Learned from Developing Whiley. Science of Computer Programming (2015), 191-220. Google ScholarGoogle ScholarDigital LibraryDigital Library
  65. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  66. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  67. Sebastian Schweizer. 2016. Lifetime Analysis for Whiley. Master's Thesis. Department of Computer Science, University of Kaiserslautern.Google ScholarGoogle Scholar
  68. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  69. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  70. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  71. Arie van Deursen, Jan Heering, and Paul Klint (Eds.). 1996. Language Prototyping: An Algebraic Specification Approach. Google ScholarGoogle ScholarDigital LibraryDigital Library
  72. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  73. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  74. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  75. 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 ScholarGoogle ScholarCross RefCross Ref

Index Terms

  1. Rewriting for sound and complete union, intersection and negation types

        Recommendations

        Comments

        Login options

        Check if you have access through your login credentials or your institution to get full access on this article.

        Sign in

        Full Access

        • Published in

          cover image ACM SIGPLAN Notices
          ACM SIGPLAN Notices  Volume 52, Issue 12
          GPCE '17
          December 2017
          258 pages
          ISSN:0362-1340
          EISSN:1558-1160
          DOI:10.1145/3170492
          Issue’s Table of Contents
          • cover image ACM Conferences
            GPCE 2017: Proceedings of the 16th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences
            October 2017
            258 pages
            ISBN:9781450355247
            DOI:10.1145/3136040

          Copyright © 2017 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: 23 October 2017

          Check for updates

          Qualifiers

          • article

        PDF Format

        View or Download as a PDF file.

        PDF

        eReader

        View online with eReader.

        eReader