Document Open Access Logo

No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System

Authors Roger Bosman , Georgios Karachalias, Tom Schrijvers

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.8.pdf
  • Filesize: 0.82 MB
  • 18 pages

Document Identifiers

Author Details

Roger Bosman
  • KU Leuven, Belgium
Georgios Karachalias
  • Tweag, Paris, France
Tom Schrijvers
  • KU Leuven, Belgium

Funding

This work was partly funded by KU Leuven project C14/20/079#55685055.

Acknowledgements

We would like to thank Steven Keuchel for their help and insights about Coq, and their comments about a draft of this paper.

Cite AsGet BibTex

Roger Bosman, Georgios Karachalias, and Tom Schrijvers. No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.8

Abstract

The Hindley-Damas-Milner (HDM) system provides polymorphism, a key feature of functional programming languages such as Haskell and OCaml. It does so through a type inference algorithm, whose soundness and completeness have been well-studied and proven both manually (on paper) and mechanically (in a proof assistant). Earlier research has focused on the problem of inferring the type of a top-level expression. Yet, in practice, we also may wish to infer the type of subexpressions, either for the sake of elaboration into an explicitly-typed target language, or for reporting those types back to the programmer. One key difference between these two problems is the treatment of underconstrained types: in the former, unification variables that do not affect the overall type need not be instantiated. However, in the latter, instantiating all unification variables is essential, because unification variables are internal to the algorithm and should not leak into the output. We present an algorithm for the HDM system that explicitly tracks the scope of all unification variables. In addition to solving the subexpression type reconstruction problem described above, it can be used as a basis for elaboration algorithms, including those that implement elaboration-based features such as type classes. The algorithm implements input and output contexts, as well as the novel concept of full contexts, which significantly simplifies the state-passing of traditional algorithms. The algorithm has been formalised and proven sound and complete using the Coq proof assistant.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Software and its engineering → Correctness
Keywords
  • type inference
  • mechanization
  • let-polymorphism

Metrics

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

Supplementary Materials

References

  1. Brian Aydemir and Stephanie Weirich. LNgen: Tool support for locally nameless representations. Technical report, Department of Computer and Information Science, University of Pennsylvania, 2010. Google Scholar
  2. Brian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering formal metatheory. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 3-15. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328443.
  3. Gert-Jan Bottu, Ningning Xie, Koar Marntirosian, and Tom Schrijvers. Coherence of type class resolution. Proc. ACM Program. Lang., 3(ICFP):91:1-91:28, 2019. URL: https://doi.org/10.1145/3341695.
  4. Hendrik Bünder. Decoupling language and editor - the impact of the language server protocol on textual domain-specific languages. In Slimane Hammoudi, Luís Ferreira Pires, and Bran Selic, editors, Proceedings of the 7th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2019, Prague, Czech Republic, February 20-22, 2019, pages 129-140. SciTePress, 2019. URL: https://doi.org/10.5220/0007556301310142.
  5. Arthur Charguéraud. The locally nameless representation. J. Autom. Reason., 49(3):363-408, 2012. URL: https://doi.org/10.1007/s10817-011-9225-2.
  6. Dominique Clément, Joëlle Despeyroux, Th. Despeyroux, and Gilles Kahn. A simple applicative language: Mini-ml. In William L. Scherlis, John H. Williams, and Richard P. Gabriel, editors, Proceedings of the 1986 ACM Conference on LISP and Functional Programming, LFP 1986, Cambridge, Massachusetts, USA, August 4-6, 1986, pages 13-27. ACM, 1986. URL: https://doi.org/10.1145/319838.319847.
  7. Luís Damas and Robin Milner. Principal type-schemes for functional programs. In Richard A. DeMillo, editor, Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 1982, pages 207-212. ACM Press, 1982. URL: https://doi.org/10.1145/582153.582176.
  8. N.G de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381-392, 1972. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  9. Catherine Dubois and Valérie Ménissier-Morain. Certification of a type inference tool for ML: damas-milner within coq. J. Autom. Reason., 23(3-4):319-346, 1999. URL: https://doi.org/10.1023/A:1006285817788.
  10. Jana Dunfield and Neelakantan R. Krishnaswami. Complete and easy bidirectional typechecking for higher-rank polymorphism. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 429-442. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500582.
  11. Andrew Gacek. The abella interactive theorem prover (system description). In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science, pages 154-161. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71070-7_13.
  12. Jacques Garrigue. A certified implementation of ML with structural polymorphism and recursive types. Math. Struct. Comput. Sci., 25(4):867-891, 2015. URL: https://doi.org/10.1017/S0960129513000066.
  13. Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Éditeur inconnu, 1972. Google Scholar
  14. Adam Gundry, Conor McBride, and James McKinna. Type inference in context. In Venanzio Capretta and James Chapman, editors, Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, MSFP@ICFP 2010, Baltimore, MD, USA, September 25, 2010, pages 43-54. ACM, 2010. URL: https://doi.org/10.1145/1863597.1863608.
  15. Conor McBride and James McKinna. Functional pearl: i am not a number-i am a free variable. In Henrik Nilsson, editor, Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2004, Snowbird, UT, USA, September 22-22, 2004, pages 1-9. ACM, 2004. URL: https://doi.org/10.1145/1017472.1017477.
  16. Wolfgang Naraschewski and Tobias Nipkow. Type inference verified: Algorithm W in isabelle/hol. J. Autom. Reason., 23(3-4):299-318, 1999. URL: https://doi.org/10.1023/A:1006277616879.
  17. Andrey Popp, Rusty Key, Louis Roché, Oleksiy Golovko, Rudi Grinberg, Sacha Ayoun, cannorin, Ulugbek Abdullaev, Thibaut Mattio, and Max Lantas. ocaml-lsp-server 1.15.1-5.0 - opam, January 2023. URL: https://opam.ocaml.org/packages/ocaml-lsp-server/ocaml-lsp-server.1.15.1-5.0/.
  18. François Pottier. Hindley-milner elaboration in applicative style: functional pearl. In Johan Jeuring and Manuel M. T. Chakravarty, editors, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014, pages 203-212. ACM, 2014. URL: https://doi.org/10.1145/2628136.2628145.
  19. John C. Reynolds. Towards a theory of type structure. In Bernard J. Robinet, editor, Programming Symposium, Proceedings Colloque sur la Programmation, Paris, France, April 9-11, 1974, volume 19 of Lecture Notes in Computer Science, pages 408-423. Springer, 1974. URL: https://doi.org/10.1007/3-540-06859-7_148.
  20. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, and Rok Strnisa. Ott: effective tool support for the working semanticist. In Ralf Hinze and Norman Ramsey, editors, Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, October 1-3, 2007, pages 1-12. ACM, 2007. URL: https://doi.org/10.1145/1291151.1291155.
  21. Martin Sulzmann and Stefan Wehr. A dictionary-passing translation of featherweight go. In Hakjoo Oh, editor, Programming Languages and Systems - 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17-18, 2021, Proceedings, volume 13008 of Lecture Notes in Computer Science, pages 102-120. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-89051-3_7.
  22. GHC Team. Using GHCi - GHC User’s Guide 9.4.4. URL: https://downloads.haskell.org/ghc/9.4.4/docs/users_guide/index.html.
  23. The Coq Development Team. The coq proof assistant, September 2022. URL: https://doi.org/10.5281/zenodo.7313584.
  24. The Haskell IDE Team. haskell-language-server documentation. URL: https://haskell-language-server.readthedocs.io/en/latest/.
  25. Dimitrios Vytiniotis, Simon Peyton Jones, and Tom Schrijvers. Let should not be generalized. In Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI '10, pages 39-50, New York, NY, USA, 2010. Association for Computing Machinery. URL: https://doi.org/10.1145/1708016.1708023.
  26. Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad-hoc. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989, pages 60-76. ACM Press, 1989. URL: https://doi.org/10.1145/75277.75283.
  27. Stephanie Weirich. Github repository: sweirich/ott, April 2022. URL: https://github.com/sweirich/ott/tree/aa65f53ea0587223662aaad9c48cb0770549f018.
  28. Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. In Alex Aiken and Greg Morrisett, editors, Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, Louisisana, USA, January 15-17, 2003, pages 224-235. ACM, 2003. URL: https://doi.org/10.1145/604131.604150.
  29. Francesco Zappa Nardelli. A locally-nameless backend for ott, March 2009. URL: https://fzn.fr/projects/ln_ott/.
  30. 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):112:1-112:29, 2019. URL: https://doi.org/10.1145/3341716.
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