Document Open Access Logo

InferType: A Compiler Toolkit for Implementing Efficient Constraint-Based Type Inference

Authors Senxi Li , Tetsuro Yamazaki , Shigeru Chiba

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.23.pdf
  • Filesize: 1.28 MB
  • 28 pages

Document Identifiers

Author Details

Senxi Li
  • The University of Tokyo, Japan
Tetsuro Yamazaki
  • The University of Tokyo, Japan
Shigeru Chiba
  • The University of Tokyo, Japan

Funding

This work was supported by JSPS KAKENHI Grant Numbers JP20H00578 and JP24H00688.

Cite AsGet BibTex

Senxi Li, Tetsuro Yamazaki, and Shigeru Chiba. InferType: A Compiler Toolkit for Implementing Efficient Constraint-Based Type Inference. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 23:1-23:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.23

Abstract

Supporting automatic type inference is in demand in modern language development. It is a challenging task but without appropriate supporting toolkits. This paper presents InferType, a Java library that helps implement constraint-based type inference. A compiler writer uses InferType’s classes and methods to describe type constraints and typing rules for type inference. InferType then performs constraint solving by translation to the Z3 SMT solver. InferType is equipped with our developed optimization technique. It reduces the search space for type variables by pre-computing the structures of those type variables for mitigating the performance bottleneck of constraint solving with deeply nested types. We use InferType to implement type inference for a subset of Python, and conduct experiments to evaluate how the developed optimization technique can affect the performance of type inference. Our results show that InferType’s optimization can greatly mitigate the performance bottleneck for programs with deeply nested types, and can potentially improve the performance for large nested types.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Domain specific languages
  • Theory of computation → Type theory
Keywords
  • Domain Specific Languages
  • Compilation
  • Static Analysis
  • Type Inference
  • Constraint Solving
  • SMT Solver

Metrics

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

Supplementary Materials

References

  1. Hendrik Antwerpen, Pierre Neron, Andrew Tolmach, Eelco Visser, and Guido Wachsmuth. A constraint language for static semantic analysis based on scope graphs. In Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 49-60, January 2016. URL: https://doi.org/10.1145/2847538.2847543.
  2. Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A Versatile and Industrial-Strength SMT Solver. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 415-442, Cham, 2022. Springer International Publishing. Google Scholar
  3. Clark Barrett, Aaron Stump, Cesare Tinelli, et al. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK), volume 13, page 14, 2010. Google Scholar
  4. Clark Barrett and Cesare Tinelli. Satisfiability Modulo Theories, pages 305-343. Springer International Publishing, Cham, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_11.
  5. Stephen Chang, Alex Knauth, and Ben Greenman. Type Systems as Macros. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL '17, pages 694-705, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3009837.3009886.
  6. Luis Damas and Robin Milner. Principal Type-Schemes for Functional Programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '82, pages 207-212, New York, NY, USA, 1982. Association for Computing Machinery. URL: https://doi.org/10.1145/582153.582176.
  7. Leonardo De Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'08/ETAPS'08, pages 337-340, Berlin, Heidelberg, 2008. Springer-Verlag. Google Scholar
  8. David Déharbe, Pascal Fontaine, Stephan Merz, and Bruno Woltzenlogel Paleo. Exploiting Symmetry in SMT Problems. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, Automated Deduction - CADE-23, pages 222-236, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  9. Bruno Dutertre. Yices 2.2. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification, pages 737-744, Cham, 2014. Springer International Publishing. Google Scholar
  10. Sven Efftinge, Moritz Eysholdt, Jan Köhnlein, Sebastian Zarnekow, Robert von Massow, Wilhelm Hasselbring, and Michael Hanus. Xbase: Implementing Domain-Specific Languages for Java. SIGPLAN Not., 48(3):112-121, September 2012. URL: https://doi.org/10.1145/2480361.2371419.
  11. Moritz Eysholdt and Heiko Behrens. Xtext: Implement Your Language Faster than the Quick and Dirty Way. In Proceedings of the ACM International Conference Companion on Object Oriented Programming Systems Languages and Applications Companion, OOPSLA '10, pages 307-309, New York, NY, USA, 2010. Association for Computing Machinery. URL: https://doi.org/10.1145/1869542.1869625.
  12. Martin Fowler and R Parsons. Addison-Wesley signature, Domain specific languages . Massachussets, 2010. Google Scholar
  13. google. pytype, 2021. URL: https://google.github.io/pytype/.
  14. Mostafa Hassan, Caterina Urban, Marco Eilers, and Peter Müller. MaxSMT-Based Type Inference for Python 3. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification, pages 12-19, Cham, 2018. Springer International Publishing. Google Scholar
  15. R. Hindley. The Principal Type-Scheme of an Object in Combinatory Logic. Transactions of the American Mathematical Society, 146:29-60, 1969. URL: http://www.jstor.org/stable/1995158.
  16. Donald B. Johnson. A Note on Dijkstra’s Shortest Path Algorithm. J. ACM, 20(3):385-388, July 1973. URL: https://doi.org/10.1145/321765.321768.
  17. Egor George Karpenkov, Karlheinz Friedberger, and Dirk Beyer. JavaSMT: A Unified Interface for SMT Solvers in Java. In Sandrine Blazy and Marsha Chechik, editors, Verified Software. Theories, Tools, and Experiments, pages 139-148, Cham, 2016. Springer International Publishing. Google Scholar
  18. Lennart C.L. Kats and Eelco Visser. The Spoofax Language Workbench: Rules for Declarative Specification of Languages and IDEs. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '10, pages 444-463, New York, NY, USA, 2010. Association for Computing Machinery. URL: https://doi.org/10.1145/1869459.1869497.
  19. Milod Kazerounian, Brianna M. Ren, and Jeffrey S. Foster. Sound, Heuristic Type Annotation Inference for Ruby. In Proceedings of the 16th ACM SIGPLAN International Symposium on Dynamic Languages, DLS 2020, pages 112-125, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3426422.3426985.
  20. Kevin Knight. Unification: A Multidisciplinary Survey. ACM Comput. Surv., 21(1):93-124, March 1989. URL: https://doi.org/10.1145/62029.62030.
  21. Jukka Lehtosalo, Guido van Rossum, and Ivan Levkivskyi. mypy, June 2012. URL: http://mypy-lang.org/.
  22. John R. Levine, Tony Mason, and Doug Brown. Lex & Yacc (2nd Ed.). O'Reilly & Associates, Inc., USA, 1992. Google Scholar
  23. Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348-375, 1978. URL: https://doi.org/10.1016/0022-0000(78)90014-4.
  24. Raphaël Monat, Abdelraouf Ouadjaout, and Antoine Miné. Static Type Analysis by Abstract Interpretation of Python Programs. In Robert Hirschfeld and Tobias Pape, editors, 34th European Conference on Object-Oriented Programming (ECOOP 2020), volume 166 of Leibniz International Proceedings in Informatics (LIPIcs), pages 17:1-17:29, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2020.17.
  25. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Syntax-Guided Quantifier Instantiation. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 145-163, Cham, 2021. Springer International Publishing. Google Scholar
  26. Martin Odersky, Christoph Zenger, and Matthias Zenger. Colored Local Type Inference. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '01, pages 41-53, New York, NY, USA, 2001. Association for Computing Machinery. URL: https://doi.org/10.1145/360204.360207.
  27. Lionel Parreaux. The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl). Proc. ACM Program. Lang., 4(ICFP), August 2020. URL: https://doi.org/10.1145/3409006.
  28. Zvonimir Pavlinovic, Tim King, and Thomas Wies. Finding Minimum Type Error Sources. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA '14, pages 525-542, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2660193.2660230.
  29. Yun Peng, Cuiyun Gao, Zongjie Li, Bowei Gao, David Lo, Qirun Zhang, and Michael Lyu. Static Inference Meets Deep Learning: A Hybrid Type Inference Approach for Python. In Proceedings of the 44th International Conference on Software Engineering, ICSE '22, pages 2019-2030, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3510003.3510038.
  30. Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for GADTs. SIGPLAN Not., 41(9):50-61, September 2006. URL: https://doi.org/10.1145/1160074.1159811.
  31. Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 1st edition, 2002. Google Scholar
  32. Benjamin C. Pierce and David N. Turner. Local Type Inference. ACM Trans. Program. Lang. Syst., 22(1):1-44, January 2000. URL: https://doi.org/10.1145/345099.345100.
  33. François Pottier. A Framework for Type Inference with Subtyping. SIGPLAN Not., 34(1):228-238, September 1998. URL: https://doi.org/10.1145/291251.289448.
  34. François Pottier and Yann Régis-Gianas. Stratified type inference for generalized algebraic data types. SIGPLAN Not., 41(1):232-244, January 2006. URL: https://doi.org/10.1145/1111320.1111058.
  35. Francois Pottier and Didier Remy. The Essence of ML Type Inference, pages 389-489. MIT press, January 2005. URL: https://doi.org/10.7551/mitpress/1104.003.0016.
  36. Ruchir Puri, David S. Kung, Geert Janssen, Wei Zhang, Giacomo Domeniconi, Vladimir Zolotov, Julian Dolby, Jie Chen, Mihir Choudhury, Lindsey Decker, Veronika Thost, Luca Buratti, Saurabh Pujar, Shyam Ramji, Ulrich Finkler, Susan Malaika, and Frederick Reiss. CodeNet: A Large-Scale AI for Code Dataset for Learning a Diversity of Coding Tasks, 2021. URL: https://arxiv.org/abs/2105.12655.
  37. J Alan Robinson. Computational logic: The unification computation. Machine intelligence, 6:63-72, 1971. Google Scholar
  38. Michael I. Schwartzbach. Type inference with inequalities. In S. Abramsky and T. S. E. Maibaum, editors, TAPSOFT '91, pages 441-455, Berlin, Heidelberg, 1991. Springer Berlin Heidelberg. Google Scholar
  39. Tatsurou Sekiguchi and Akinori Yonezawa. A complete type inference system for subtyped recursive types. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, pages 667-686, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg. Google Scholar
  40. Jeremy Siek and Walid Taha. Gradual Typing for Objects. In Erik Ernst, editor, ECOOP 2007 - Object-Oriented Programming, pages 2-27, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  41. Richard M. Stallman. Bison: The Yacc-Compatible Parser Generator, 2015. URL: https://api.semanticscholar.org/CorpusID:60543798.
  42. Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin. Dependent Types and Multi-Monadic Effects in F*. SIGPLAN Not., 51(1):256-270, January 2016. URL: https://doi.org/10.1145/2914770.2837655.
  43. Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, and Eelco Visser. Scopes as Types. Proc. ACM Program. Lang., 2(OOPSLA), October 2018. URL: https://doi.org/10.1145/3276484.
  44. Niki Vazou, Eric L. Seidel, and Ranjit Jhala. LiquidHaskell: Experience with Refinement Types in the Real World. SIGPLAN Not., 49(12):39-51, September 2014. URL: https://doi.org/10.1145/2775050.2633366.
  45. Markus Voelter and Vaclav Pech. Language Modularity with the MPS Language Workbench. In Proceedings of the 34th International Conference on Software Engineering, ICSE '12, pages 1449-1450. IEEE Press, 2012. Google Scholar
  46. Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann. OUTSIDEIN(X): modular type inference with local assumptions. J. Funct. Program., 21:333-412, September 2011. URL: https://doi.org/10.1017/S0956796811000098.
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