Document Open Access Logo

Elementary Type Inference

Authors Jinxu Zhao, Bruno C. d. S. Oliveira

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.2.pdf
  • Filesize: 0.89 MB
  • 28 pages

Document Identifiers

Author Details

Jinxu Zhao
  • Department of Computer Science, The University of Hong Kong, China
Bruno C. d. S. Oliveira
  • Department of Computer Science, The University of Hong Kong, China

Funding

The research is supported by the Type Inference for Complex Type Systems collaboration project (TC20210422012) between Huawei, and the University of Hong Kong and Hong Kong Research Grants Council projects number 17209520 and 17209821.

Acknowledgements

We are grateful to the anonymous reviewers for their valuable comments which helped to improve the presentation of this work. We also thank Chen Cui for creating the implementation for our prototype.

Cite AsGet BibTex

Jinxu Zhao and Bruno C. d. S. Oliveira. Elementary Type Inference. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 2:1-2:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECOOP.2022.2

Abstract

Languages with polymorphic type systems are made convenient to use by employing type inference to avoid redundant type information. Unfortunately, features such as impredicative types and subtyping make complete type inference very challenging or impossible to realize. This paper presents a form of partial type inference called elementary type inference. Elementary type inference adopts the idea of inferring only monotypes from past work on predicative higher-ranked polymorphism. This idea is extended with the addition of explicit type applications that work for any polytypes. Thus easy (predicative) instantiations can be inferred, while all other (impredicative) instantiations are always possible with explicit type applications without any compromise in expressiveness. Our target is a System F extension with top and bottom types, similar to the language employed by Pierce and Turner in their seminal work on local type inference. We show a sound, complete and decidable type system for a calculus called F_{< :}^e, that targets that extension of System F. A key design choice in F_{< :}^e is to consider top and bottom types as polytypes only. An important technical challenge is that the combination of predicative implicit instantiation and impredicative explicit type applications, in the presence of standard subtyping rules, is non-trivial. Without some restrictions, key properties, such as subsumption and stability of type substitution lemmas, break. To address this problem we introduce a variant of polymorphic subtyping called stable subtyping with some mild restrictions on implicit instantiation. All the results are mechanically formalized in the Abella theorem prover.

Subject Classification

ACM Subject Classification
  • Software and its engineering → General programming languages
Keywords
  • Type Inference

Metrics

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

Related Versions

Supplementary Materials

References

  1. Gert-Jan Bottu and Richard A. Eisenberg. Seeking stability by being lazy and shallow: Lazy and shallow instantiation is user friendly. In Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell, pages 85-97, New York, NY, USA, 2021. Association for Computing Machinery. Google Scholar
  2. L. Cardelli, S. Martini, J.C. Mitchell, and A. Scedrov. An extension of system F with subtyping. Information and Computation, 109(1):4-56, 1994. Google Scholar
  3. Jacek Chrząszcz. Polymorphic subtyping without distributivity. In Luboš Brim, Jozef Gruska, and Jiří Zlatuška, editors, Mathematical Foundations of Computer Science 1998, pages 346-355, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg. Google Scholar
  4. Maurizio Cimadamore. Jep 101: Generalized target-type inference, 2015. URL: http://openjdk.java.net/jeps/101.
  5. 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, 1982. Google Scholar
  6. Stephen Dolan and Alan Mycroft. Polymorphism, subtyping, and type inference in MLsub. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 60-72, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3009837.3009882.
  7. Jana Dunfield. Elaborating intersection and union types. J. Funct. Program., 24(2-3):133-165, 2014. URL: https://doi.org/10.1017/S0956796813000270.
  8. Jana Dunfield and Neelakantan R. Krishnaswami. Complete and easy bidirectional typechecking for higher-rank polymorphism. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP '13, 2013. Google Scholar
  9. Jana Dunfield and Neelakantan R. Krishnaswami. Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types. PACMPL, (POPL), January 2019. URL: http://arxiv.org/abs/1601.05106.
  10. Jana Dunfield and Neelakantan R. Krishnaswami. Bidirectional typing. ACM Comput. Surv., 54(5), May 2021. Google Scholar
  11. Jonathan Eifrig, Scott Smith, and Valery Trifonov. Sound polymorphic type inference for objects. In Proceedings of the Tenth Annual Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA 1995, Austin, Texas, USA, October 15-19, 1995, OOPSLA '95, pages 169-184, New York, NY, USA, 1995. Association for Computing Machinery. URL: https://doi.org/10.1145/217838.217858.
  12. Jonathan Eifrig, Scott Smith, and Valery Trifonov. Type inference for recursively constrained types and its application to OOP. Electronic Notes in Theoretical Computer Science, 1:132-153, 1995. MFPS XI, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference. URL: https://doi.org/10.1016/S1571-0661(04)80008-2.
  13. Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed. Visible type application. In Peter Thiemann, editor, Programming Languages and Systems, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg. Google Scholar
  14. Frank Emrich, Sam Lindley, Jan Stolarek, James Cheney, and Jonathan Coates. Freezeml: Complete and easy type inference for first-class polymorphism. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020, pages 423-437. Association for Computing Machinery, 2020. Google Scholar
  15. Andrew Gacek. The Abella interactive theorem prover (system description). In Proceedings of IJCAR 2008, Lecture Notes in Artificial Intelligence, 2008. Google Scholar
  16. Roger Hindley. The principal type-scheme of an object in combinatory logic. Transactions of the american mathematical society, 146:29-60, 1969. Google Scholar
  17. Didier Le Botlan and Didier Rémy. MLF: Raising ML to the power of system F. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP '03, 2003. Google Scholar
  18. Daan Leijen. HMF: Simple type inference for first-class polymorphism. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP '08, 2008. Google Scholar
  19. Robin Milner. A theory of type polymorphism in programming. Journal of computer and system sciences, 17(3):348-375, 1978. Google Scholar
  20. Martin Odersky and Konstantin Läufer. Putting type annotations to work. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '96, 1996. Google Scholar
  21. 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. Google Scholar
  22. Bruno C.d.S. Oliveira, Adriaan Moors, and Martin Odersky. Type classes as objects and implicits. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '10, pages 341-360, 2010. Google Scholar
  23. 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.
  24. Simon Peyton Jones and Mark Shields. Lexically-scoped type variables. Draft, 2004. URL: http://research.microsoft.com/en-us/um/people/simonpj/papers/scoped-tyvars/.
  25. Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical type inference for arbitrary-rank types. Journal of functional programming, 17(1):1-82, 2007. Google Scholar
  26. Peyton Jones, Simon. Simplify Subsumption. GHC Proposals, 2020. URL: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst.
  27. Benjamin C. Pierce and David N. Turner. Local type inference. ACM Trans. Program. Lang. Syst., 22(1):1-44, January 2000. Google Scholar
  28. Hubert Plociniczak. Decrypting Local Type Inference. PhD thesis, EPFL, 2016. Google Scholar
  29. François Pottier and Didier Rémy. Advanced Topics in Types and Programming Languages, chapter The Essence of ML Type Inference, pages 387-489. The MIT Press, 2005. Google Scholar
  30. François Pottier. Type inference in the presence of subtyping: from theory to practice. PhD thesis, INRIA, 1998. Google Scholar
  31. Tom Schrijvers, Bruno C. d. S. Oliveira, Philip Wadler, and Koar Marntirosian. COCHIS: Stable and coherent implicits. Journal of Functional Programming, 29:e3, 2019. Google Scholar
  32. Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis. A quick look at impredicativity. Proc. ACM Program. Lang., 4(ICFP), August 2020. Google Scholar
  33. Alejandro Serrano, Jurriaan Hage, Dimitrios Vytiniotis, and Simon Peyton Jones. Guarded impredicative polymorphism. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, 2018. Google Scholar
  34. Zhendong Su, Alexander Aiken, Joachim Niehren, Tim Priesnitz, and Ralf Treinen. The first-order theory of subtyping constraints. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '02, pages 203-216, New York, NY, USA, 2002. Association for Computing Machinery. URL: https://doi.org/10.1145/503272.503292.
  35. Jerzy Tiuryn and Pawel Urzyczyn. The subtyping problem for second-order types is undecidable. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 1996. Google Scholar
  36. Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. FPH: First-class polymorphism for Haskell. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP '08, 2008. Google Scholar
  37. P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '89, pages 60-76, New York, NY, USA, 1989. Association for Computing Machinery. Google Scholar
  38. Joe B Wells. Typability and type checking in system F are equivalent and undecidable. Annals of Pure and Applied Logic, 98(1-3):111-156, 1999. Google Scholar
  39. Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. A mechanical formalization of higher-ranked polymorphic type inference. Proc. ACM Program. Lang., 3(ICFP), July 2019. 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