Document Open Access Logo

Static Typing of Complex Presence Constraints in Interfaces

Authors Nathalie Oostvogels, Joeri De Koster, Wolfgang De Meuter

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2018.14.pdf
  • Filesize: 0.62 MB
  • 27 pages

Document Identifiers

Author Details

Nathalie Oostvogels
  • Vrije Universiteit Brussel, Brussels, Belgium
Joeri De Koster
  • Vrije Universiteit Brussel, Brussels, Belgium
Wolfgang De Meuter
  • Vrije Universiteit Brussel, Brussels, Belgium

Funding

  • Oostvogels, Nathalie: Funded by a PhD Fellowship of the Research Foundation - Flanders (FWO)

Cite AsGet BibTex

Nathalie Oostvogels, Joeri De Koster, and Wolfgang De Meuter. Static Typing of Complex Presence Constraints in Interfaces. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 14:1-14:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.ECOOP.2018.14

Abstract

Many functions in libraries and APIs have the notion of optional parameters, which can be mapped onto optional properties of an object representing those parameters. The fact that properties are optional opens up the possibility for APIs and libraries to design a complex "dependency logic" between properties: for example, some properties may be mutually exclusive, some properties may depend on others, etc. Existing type systems are not strong enough to express such dependency logic, which can lead to the creation of invalid objects and accidental usage of absent properties. In this paper we propose TypeScriptIPC: a variant of TypeScript with a novel type system that enables programmers to express complex presence constraints on properties. We prove that it is sound with respect to enforcing complex dependency logic defined by the programmer when an object is created, modified or accessed.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Software and its engineering → Object oriented languages
  • Software and its engineering → Data types and structures
Keywords
  • type checking
  • interfaces
  • dependency logic

Metrics

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

Supplementary Materials

References

  1. Hack. URL: http://hacklang.org/.
  2. TypeScript 2.0 Release Notes. URL: https://www.typescriptlang.org/docs/handbook/release-notes/typescript-2-0.html.
  3. Martin Abadi and Luca Cardelli. A theory of objects. Springer Science &Business Media, 2012. Google Scholar
  4. Christopher Anderson, Paola Giannini, and Sophia Drossopoulou. Towards type inference for JavaScript. In European conference on Object-oriented programming, pages 428-452. Springer, 2005. Google Scholar
  5. Lennart Augustsson. Cayenne: a language with dependent types. In Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, ICFP '98, pages 239-250, New York, NY, USA, 1998. ACM. Google Scholar
  6. Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D Gordon, and Sergio Maffeis. Refinement types for secure implementations. ACM Transactions on Programming Languages and Systems (TOPLAS), 33(2):8, 2011. Google Scholar
  7. Gavin Bierman, Martín Abadi, and Mads Torgersen. Understanding TypeScript. In European Conference on Object-Oriented Programming, pages 257-281. Springer, 2014. Google Scholar
  8. Gavin M Bierman, MJ Parkinson, and AM Pitts. MJ: An imperative core calculus for Java and Java with effects. Technical report, University of Cambridge, Computer Laboratory, 2003. Google Scholar
  9. Satish Chandra, Colin S Gordon, Jean-Baptiste Jeannin, Cole Schlesinger, Manu Sridharan, Frank Tip, and Youngil Choi. Type inference for static compilation of JavaScript. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 410-429. ACM, 2016. Google Scholar
  10. Avik Chaudhuri, Panagiotis Vekris, Sam Goldman, Marshall Roch, and Gabriel Levi. Fast and precise type checking for JavaScript. Proceedings of the ACM on Programming Languages, 1(OOPSLA):48, 2017. Google Scholar
  11. Ravi Chugh, David Herman, and Ranjit Jhala. Dependent Types for JavaScript. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '12, pages 587-606, New York, NY, USA, 2012. ACM. Google Scholar
  12. Manuel Fähndrich and K. Rustan M. Leino. Declaring and Checking Non-null Types in an Object-oriented Language. In Proceedings of the 18th Annual ACM SIGPLAN Conference on Object-oriented Programing, Systems, Languages, and Applications, OOPSLA '03, pages 302-312, New York, NY, USA, 2003. ACM. Google Scholar
  13. Cormac Flanagan, Stephen N Freund, and Aaron Tomb. Hybrid types, invariants, and refinements for imperative objects. FOOL/WOOD, 6, 2006. Google Scholar
  14. Tim Freeman and Frank Pfenning. Refinement Types for ML. In In Proceedings of the SIGPLAN'91 Symposium on Language Design and Implementation. Citeseer, 1991. Google Scholar
  15. Jean H Gallier. Logic for computer science: foundations of automatic theorem proving. Courier Dover Publications, 2015. Google Scholar
  16. Jean-Yves Girard. Linear logic. Theoretical computer science, 50(1):1-101, 1987. Google Scholar
  17. Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. Typing Local Control and State Using Flow Analysis. In European Symposium on Programming, pages 256-275. Springer, 2011. Google Scholar
  18. Phillip Heidegger and Peter Thiemann. Recency types for analyzing scripting languages. In European conference on Object-oriented programming, pages 200-224. Springer, 2010. Google Scholar
  19. Thomas S Heinze, Anders Møller, and Fabio Strocco. Type safety analysis for Dart. In Proceedings of the 12th Symposium on Dynamic Languages, pages 1-12. ACM, 2016. Google Scholar
  20. Vineeth Kashyap, John Sarracino, John Wagner, Ben Wiedermann, and Ben Hardekopf. Type Refinement for Static Analysis of JavaScript. In Proceedings of the 9th Symposium on Dynamic Languages, DLS '13, pages 17-26, New York, NY, USA, 2013. ACM. Google Scholar
  21. Andrew M. Kent, David Kempe, and Sam Tobin-Hochstadt. Occurrence Typing Modulo Theories. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '16, pages 296-309, New York, NY, USA, 2016. ACM. Google Scholar
  22. Per Martin-Löf and Giovanni Sambin. Intuitionistic type theory, volume 9. Bibliopolis Napoli, 1984. Google Scholar
  23. Nathaniel Nystrom, Vijay Saraswat, Jens Palsberg, and Christian Grothoff. Constrained types for object-oriented languages. In In OOPSLA’08: Proceedings of the 23rd ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications. Citeseer, 2008. Google Scholar
  24. Nathalie Oostvogels, Joeri De Koster, and Wolfgang De Meuter. Inter-parameter Constraints in Contemporary Web APIs. In International Conference on Web Engineering, pages 323-335. Springer, 2017. Google Scholar
  25. Matthew M Papi, Mahmood Ali, Telmo Luis Correa Jr, Jeff H Perkins, and Michael D Ernst. Practical pluggable types for Java. In Proceedings of the 2008 international symposium on Software testing and analysis, pages 201-212. ACM, 2008. Google Scholar
  26. Garrel Pottinger. A type assignment for the strongly normalizable λ-terms. To HB Curry: essays on combinatory logic, lambda calculus and formalism, pages 561-577, 1980. Google Scholar
  27. Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin Bierman, and Panagiotis Vekris. Safe &Efficient Gradual Typing for TypeScript. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 167-180, New York, NY, USA, 2015. ACM. Google Scholar
  28. Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek. Concrete types for TypeScript. In LIPIcs-Leibniz International Proceedings in Informatics, volume 37. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  29. Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. Liquid types. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '08, pages 159-169, New York, NY, USA, 2008. ACM. Google Scholar
  30. Francesca Rossi, Peter Van Beek, and Toby Walsh. Handbook of constraint programming. Elsevier, 2006. Google Scholar
  31. Peter Thiemann. Towards a type system for analyzing javascript programs. In European Symposium On Programming, pages 408-422. Springer, 2005. Google Scholar
  32. Sam Tobin-Hochstadt and Matthias Felleisen. The Design and Implementation of Typed Scheme. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '08, pages 395-406, New York, NY, USA, 2008. ACM. Google Scholar
  33. Sam Tobin-Hochstadt and Matthias Felleisen. Logical Types for Untyped Languages. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP '10, pages 117-128, New York, NY, USA, 2010. ACM. Google Scholar
  34. Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala. Refinement Types for TypeScript. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '16, pages 310-325, New York, NY, USA, 2016. ACM. Google Scholar
  35. Hongwei Xi and Frank Pfennig. Eliminating Array Bound Checking Through Dependent Types. In In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, 1998. Google Scholar
  36. Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 214-227. ACM, 1999. 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 Imprint Privacy Contact