Type Inference Logics
Article No.: 346, Pages 2125 - 2155
Abstract
Type inference is essential for statically-typed languages such as OCaml and Haskell. It can be decomposed into two (possibly interleaved) phases: a generator converts programs to constraints; a solver decides whether a constraint is satisfiable. Elaboration, the task of decorating a program with explicit type annotations, can also be structured in this way. Unfortunately, most machine-checked implementations of type inference do not follow this phase-separated, constraint-based approach. Those that do are rarely executable, lack effectful abstractions, and do not include elaboration. To close the gap between common practice in real-world implementations and mechanizations inside proof assistants, we propose an approach that enables modular reasoning about monadic constraint generation in the presence of elaboration. Our approach includes a domain-specific base logic for reasoning about metavariables and a program logic that allows us to reason abstractly about the meaning of constraints. To evaluate it, we report on a machine-checked implementation of our techniques inside the Coq proof assistant. As a case study, we verify both soundness and completeness for three elaborating type inferencers for the simply typed lambda calculus with Booleans. Our results are the first demonstration that type inference algorithms can be verified in the same form as they are implemented in practice: in an imperative style, modularly decomposed into constraint generation and solving, and delivering elaborated terms to the remainder of the compiler chain.
References
[1]
Michael Abbott, Thorsten Altenkirch, and Neil Ghani. 2003. Categories of Containers. In Foundations of Software Science and Computation Structures (FoSSaCS’03), Andrew D. Gordon (Ed.). Springer, 23–38. isbn:978-3-540-36576-1
[2]
Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy. 2017. Dijkstra monads for free. In Principles of Programming Languages (POPL). 515–529. https://arxiv.org/abs/1608.06499
[3]
Ki Yung Ahn and Andrea Vezzosi. 2016. Executable Relational Specifications of Polymorphic Type Systems Using Prolog. In Functional and Logic Programming (Lecture Notes in Computer Science, Vol. 9613). Springer, 109–125.
[4]
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. 2018. A type and scope safe universe of syntaxes with binding: their semantics and proofs. Proc. ACM Program. Lang. 2, ICFP, Article 90 (jul 2018), 30 pages.
[5]
Thorsten Altenkirch and Bernhard Reus. 1999. Monadic Presentations of Lambda Terms Using Generalized Inductive Types. In Computer Science Logic, Jörg Flum and Mario Rodriguez-Artalejo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 453–468. isbn:978-3-540-48168-3
[6]
Krzysztof R. Apt. 1983. Ten years of Hoare’s logic: A survey—part II: Nondeterminism. Theoretical Computer Science 28, 1 (1983), 83–109. issn:0304-3975
[7]
Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, and Laurent Théry. 2010. Extending Coq with Imperative Features and Its Application to SAT Verification. In Interactive Theorem Proving, Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 83–98. isbn:978-3-642-14052-5
[8]
Kenichi Asai and Kyoko Kadowaki. 2017. A Type Theoretic Specification of Type Inference. (2017). http://pllab.is.ocha.ac.jp/~asai/papers/paper2017.pdf Unpublished.
[9]
Franz Baader, Wayne Snyder, Paliath Narendran, Manfred Schmidt-Schauss, and Klaus Schulz. 2001. Chapter 8 - Unification Theory. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.). North-Holland, Amsterdam. isbn:978-0-444-50813-3
[10]
Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser. 2017. Intrinsically-Typed Definitional Interpreters for Imperative Languages. Proc. ACM Program. Lang. 2, POPL, Article 16 (dec 2017), 34 pages.
[11]
Marcin Benke, Peter Dybjer, and Patrik Jansson. 2003. Universes for generic programs and proofs in dependent type theory. Nordic J. of Computing 10, 4 (Dec. 2003), 265–289. issn:1236-6064 http://dl.acm.org/citation.cfm?id=985799.985801
[12]
Nick Benton, Chung-Kil Hur, Andrew J. Kennedy, and Conor McBride. 2012. Strongly Typed Term Representations in Coq. J. Autom. Reason. 49, 2 (aug 2012), 141–159. issn:0168-7433
[13]
Roger Bosman, Georgios Karachalias, and Tom Schrijvers. 2023. No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System. In 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31-August 4, 2023, Białystok, Poland (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://drops.dagstuhl.de/opus/volltexte/2023/18383/
[14]
Luca Cardelli. 1987. Basic polymorphic typechecking. Science of Computer Programming 8, 2 (1987), 147–172.
[15]
Denis Carnier, François Pottier, and Steven Keuchel. 2024. Type Inference Logics - Artifact.
[16]
Denis Carnier, François Pottier, and Steven Keuchel. 2024. Type Inference Logics - Software Repository. https://github.com/decrn/tilogics
[17]
Joris Ceulemans, Andreas Nuys, and Dominique Devriese. 2022. Sikkel: Multimode Simply Type Theory as an Agda Library. In Workshop on Mathematically Structured Functional Programming (MSFP). 93–112.
[18]
David Cock, Gerwin Klein, and Thomas Sewell. 2008. Secure Microkernels, State Monads and Scalable Refinement. In Theorem Proving in Higher Order Logics, Otmane Ait Mohamed, César Mu noz, and Sofiène Tahar (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 167–182. isbn:978-3-540-71067-7
[19]
Haskell B. Curry and Robert M. Feys. 1958. Combinatory Logic. Vol. 1. North-Holland Publishing Company, Amsterdam.
[20]
Luis Damas. 1984. Type Assignment in Programming Languages. Ph. D. Dissertation. University of Edinburgh. http://hdl.handle.net/1842/13555
[21]
Luis Damas and Robin Milner. 1982. Principal type-schemes for functional programs. In Principles of Programming Languages (POPL). 207–212.
[22]
Rowan Davies and Frank Pfenning. 2001. A Modal Analysis of Staged Computation. J. ACM 48, 3 (may 2001), 555–604. issn:0004-5411
[23]
Catherine Dubois and Valérie Ménissier-Morain. 1999. Certification of a Type Inference Tool for ML: Damas-Milner within Coq. Journal of Automated Reasoning 23, 3–4 (Nov. 1999), 319–346. http://www.ensiie.fr/~dubois/jar_final.pdf
[24]
Jana Dunfield. 2009. Greedy Bidirectional Polymorphism. In Proceedings of the 2009 ACM SIGPLAN Workshop on ML (Edinburgh, Scotland) (ML ’09). Association for Computing Machinery, New York, NY, USA, 15–26. isbn:9781605585093
[25]
Jana Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and easy bidirectional typechecking for higher-rank polymorphism. In International Conference on Functional Programming (ICFP). 429–442.
[26]
Nicola Gambino and Martin Hyland. 2004. Wellfounded Trees and Dependent Polynomial Functors. In Types for Proofs and Programs (LNCS, Vol. 3085), Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer, 210–225. isbn:978-3-540-24849-1
[27]
Jacques Garrigue. 2015. A certified implementation of ML with structural polymorphism and recursive types. Mathematical Structures in Computer Science 25, 4 (2015), 867–891. https://www.math.nagoya-u.ac.jp/~garrigue/papers/certint1202.pdf
[28]
Adam Gundry, Conor McBride, and James McKinna. 2010. Type inference in context. In Workshop on Mathematically Structured Functional Programming (MSFP). 43–54. https://adam.gundry.co.uk/pub/type-inference-in-context/
[29]
Jörgen Gustavsson and Josef Svenningsson. 2001. Constraint Abstractions. In Symposium on Programs as Data Objects (Lecture Notes in Computer Science, Vol. 2053). Springer. http://www.cse.chalmers.se/~josefs/publications/ca.pdf
[30]
Peter Hancock and Anton Setzer. 2000. Interactive Programs in Dependent Type Theory. In Computer Science Logic, Peter G. Clote and Helmut Schwichtenberg (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 317–331. isbn:978-3-540-44622-4
[31]
Bastiaan Heeren, Jurriaan Hage, and S. Doaitse Swierstra. 2003. Scripting the type inference process. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003, Colin Runciman and Olin Shivers (Eds.). ACM, 3–13.
[32]
Ralf Hinze. 2000. Generic programs and proofs. Habilitation thesis. Universität Bonn.
[33]
Mauro Jaskelioff and Ondrej Rypacek. 2012. An Investigation of the Laws of Traversals. In Proceedings of the Fourth Workshop on Mathematically Structured Functional Programming, MSFP’12 (Electronic Proceedings in Theoretical Computer Science, Vol. 76), James Chapman and Paul Blain Levy (Eds.). Open Publishing Association, 40–49.
[34]
Jean-Pierre Jouannaud and Claude Kirchner. 1991. Solving equations in abstract algebras: a rule-based survey of unification. In Computational Logic. Essays in honor of Alan Robinson, Jean-Louis Lassez and Gordon Plotkin (Eds.). MIT Press, Chapter 8, 257–321.
[35]
Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. In International Conference on Functional Programming (ICFP). 256–269. http://iris-project.org/pdfs/2016-icfp-iris2-final.pdf
[36]
Hrutvik Kanabar. 2023. Verified compilation of a purely functional language to a realistic machine semantics. Ph. D. Dissertation. School of Computing, University of Kent. https://hrutvik.co.uk/assets/pdf/Hrutvik_Kanabar_thesis.pdf
[37]
Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, and Riccardo Zanetti. 2023. PureCake: A Verified Compiler for a Lazy Functional Language. Proceedings of the ACM on Programming Languages 7, PLDI (2023), 952–976.
[38]
Chantal Keller and Thorsten Altenkirch. 2010. Hereditary Substitutions for Simple Types, Formalized. In Proceedings of the Third ACM SIGPLAN Workshop on Mathematically Structured Functional Programming (Baltimore, Maryland, USA) (MSFP ’10). Association for Computing Machinery, New York, NY, USA, 3–10. isbn:9781450302555
[39]
Steven Keuchel, Sander Huyghebaert, Georgy Lukyanov, and Dominique Devriese. 2022. Verified Symbolic Execution with Kripke Specification Monads (and No Meta-Programming). Proc. ACM Program. Lang. 6, ICFP, Article 97 (aug 2022), 31 pages.
[40]
Steven Keuchel and Johan T. Jeuring. 2012. Generic conversions of abstract syntax representations. In Proceedings of the 8th ACM SIGPLAN workshop on Generic programming, WGP ’12. ACM, 57–68. isbn:978-1-4503-1576-0 Copenhagen, Denmark, September 12, 2012.
[41]
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. 2018. MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proceedings of the ACM on Programming Languages 2, ICFP (2018), 77:1–77:30.
[42]
Robert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In Principles of Programming Languages (POPL). http://cs.au.dk/~birke/papers/ipm-conf.pdf
[43]
Ramana Kumar and Michael Norrish. 2010. (Nominal) Unification by Recursive Descent with Triangular Substitutions. In Interactive Theorem Proving, Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 51–66. isbn:978-3-642-14052-5
[44]
Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, and éric Tanter. 2019. Dijkstra monads for all. Proceedings of the ACM on Programming Languages 3, ICFP (2019), 104:1–104:29.
[45]
Olivier Martinot and Gabriel Scherer. 2020. Quantified Applicatives: API design for type-inference constraints. Presented at the ML Family Workshop.
[46]
Conor McBride. 2000. Dependently Typed Functional Programs and their Proofs. Ph. D. Dissertation. University of Edinburgh.
[47]
Conor McBride. 2002. Elimination with a Motive. In Types for Proofs and Programs, Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack, and Robert Pollack (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 197–216. isbn:978-3-540-45842-5
[48]
Conor McBride. 2003. First-Order Unification by Structural Recursion. Journal of Functional Programming 13, 6 (2003), 1061–1075.
[49]
Conor McBride. 2003. First-Order Unification by Structural Recursion – Correctness Proof. http://www.strictlypositive.org/foubsr-website/ Accessed: 2023-10-26.
[50]
Conor McBride. 2011. Functional pearl: Kleisli arrows of outrageous fortune. (2011). Available at https://personal.cis.strath.ac.uk/conor.mcbride/Kleisli.pdf.
[51]
Conor McBride and Ross Paterson. 2008. Applicative Programming with Effects. Journal of Functional Programming 18, 1 (2008), 1–13. http://www.soi.city.ac.uk/~ross/papers/Applicative.pdf
[52]
Robin Milner. 1978. A Theory of Type Polymorphism in Programming. J. Comput. System Sci. 17, 3 (Dec. 1978), 348–375.
[53]
E. Moggi, G. Bellè, and C.B. Jay. 1999. Monads, Shapely Functors and Traversals. Electronic Notes in Theoretical Computer Science 29 (1999), 187–208. issn:1571-0661 CTCS ’99, Conference on Category Theory and Computer Science.
[54]
Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual modal type theory. ACM Trans. Comput. Logic 9, 3, Article 23 (jun 2008), 49 pages. issn:1529-3785
[55]
Wolfgang Naraschewski and Tobias Nipkow. 1999. Type Inference Verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning 23 (1999), 299–318. http://www4.informatik.tu-muenchen.de/~nipkow/pubs/W.ps.gz
[56]
Dieter Nazareth and Tobias Nipkow. 1996. Formal Verification of Algorithm W: The Monomorphic Case. In Theorem Proving in Higher Order Logics (TPHOLs) (Lecture Notes in Computer Science, Vol. 1125). Springer, 331–345. https://www21.in.tum.de/~nipkow/pubs/tphol96.html
[57]
Pierre Nigron and Pierre-évariste Dagand. 2021. Reaching for the Star: Tale of a Monad in Coq. In Interactive Theorem Proving (ITP) (Leibniz International Proceedings in Informatics, Vol. 193). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 29:1–29:19.
[58]
Martin Odersky and Konstantin Läufer. 1996. Putting Type Annotations To Work. In Principles of Programming Languages (POPL). 54–67. http://lamp.epfl.ch/~odersky/papers/popl96.ps.gz
[59]
Martin Odersky, Martin Sulzmann, and Martin Wehr. 1999. Type Inference with Constrained Types. Theory and Practice of Object Systems 5, 1 (1999), 35–55.
[60]
Susan Owicki and David Gries. 1976. Verifying Properties of Parallel Programs: An Axiomatic Approach. Commun. ACM 19, 5 (may 1976), 279–285. issn:0001-0782
[61]
Frank Pfenning and Conal Elliott. 1988. Higher-Order Abstract Syntax. In Programming Language Design and Implementation (PLDI). 199–208.
[62]
François Pottier. 2014. Hindley-Milner elaboration in applicative style. In International Conference on Functional Programming (ICFP). http://cambium.inria.fr/~fpottier/publis/fpottier-elaboration.pdf
[63]
François Pottier and Didier Rémy. 2005. The Essence of ML Type Inference. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). MIT Press, Chapter 10, 389–489. http://cambium.inria.fr/~fpottier/publis/emlti-final.pdf
[64]
Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser. 2020. Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (New Orleans, LA, USA) (CPP 2020). Association for Computing Machinery, New York, NY, USA, 284–298. isbn:9781450370974
[65]
A. J. Rouvoet. 2021. Correct by Construction Language Implementations. Ph. D. Dissertation. Delft University of Technology.
[66]
Rafael Castro G. Silva, Cristiano D. Vasconcellos, and Karina Girardi Roggia. 2020. Monadic W in Coq. In Brazilian Symposium on Programming Languages (SBLP). 25–32.
[67]
Lucas Silver and Steve Zdancewic. 2021. Dijkstra monads forever: termination-sensitive specifications for interaction trees. Proceedings of the ACM on Programming Languages 5, POPL (2021), 1–28.
[68]
Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits. 2013. Verifying higher-order programs with the Dijkstra monad. ACM SIGPLAN Notices 48, 6 (2013), 387–398.
[69]
Wouter Swierstra. 2009. A Hoare Logic for the State Monad. In Theorem Proving in Higher Order Logics (TPHOLs) (Lecture Notes in Computer Science, Vol. 5674). Springer, 440–451. https://webspace.science.uu.nl/~swier004/publications/2009-tphols.pdf
[70]
Wouter Swierstra and Tim Baanen. 2019. A predicate transformer semantics for effects (functional pearl). Proceedings of the ACM on Programming Languages 3, ICFP (2019), 103:1–103:26.
[71]
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, and Michael Norrish. 2019. The verified CakeML compiler backend. Journal of Functional Programming 29 (2019), e2. https://cakeml.org/jfp19.pdf
[72]
Yong Kiam Tan, Scott Owens, and Ramana Kumar. 2015. A verified type system for CakeML. In Implementation of Functional Languages (IFL). 7:1–7:12. https://cakeml.org/ifl15.pdf
[73]
Aaron Tomb and Cormac Flanagan. 2005. Automatic type inference via partial evaluation. In Principles and Practice of Declarative Programming (PPDP). 106–116. http://alumni.soe.ucsc.edu/~atomb/tomb05inference.pdf
[74]
Christian Urban and Tobias Nipkow. 2009. Nominal verification of algorithm W. In From Semantics to Computer Science: Essays in Honour of Gilles Kahn, Yves Bertot, Gérard Huet, Jean-Jacques Lévy, and Gordon Plotkin (Eds.). Cambridge University Press, 363–382. https://www21.in.tum.de/~nipkow/pubs/w.pdf
[75]
Cas van der Rest, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser, and Peter Mosses. 2022. Intrinsically-Typed Definitional Interpreters à La Carte. Proc. ACM Program. Lang. 6, OOPSLA2, Article 192 (oct 2022), 30 pages.
[76]
Janis Voigtländer. 2008. Asymptotic Improvement of Computations over Free Monads. In Mathematics of Program Construction, Philippe Audebaud and Christine Paulin-Mohring (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 388–403. isbn:978-3-540-70594-9
[77]
Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann. 2011. OutsideIn(X): Modular type inference with local assumptions. Journal of Functional Programming 21, 4–5 (2011), 333–412. http://research.microsoft.com/en-us/um/people/simonpj/papers/constraints/jfp-outsidein.pdf
[78]
Mitchell Wand. 1987. A Simple Algorithm and Proof for Type Inference. Fundamenta Informaticæ 10 (1987), 115–122. http://web.cs.ucla.edu/~palsberg/course/cs239/reading/wand87.pdf
[79]
Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2018. Formalization of a Polymorphic Subtyping Algorithm. In Interactive Theorem Proving, Jeremy Avigad and Assia Mahboubi (Eds.). Springer International Publishing, Cham, 604–622. isbn:978-3-319-94821-8
[80]
Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. A mechanical formalization of higher-ranked polymorphic type inference. Proceedings of the ACM on Programming Languages 3, ICFP (2019), 112:1–112:29.
Index Terms
- Type Inference Logics
Recommendations
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...
Simple, partial type-inference for System F based on type-containment
Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingWe explore partial type-inference for System F based on type-containment. We consider both cases of a purely functional semantics and a call-by-value stateful semantics. To enable type-inference, we require higher-rank polymorphism to be user-specified ...
Simple, partial type-inference for System F based on type-containment
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingWe explore partial type-inference for System F based on type-containment. We consider both cases of a purely functional semantics and a call-by-value stateful semantics. To enable type-inference, we require higher-rank polymorphism to be user-specified ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2024
2691 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 08 October 2024
Published in PACMPL Volume 8, Issue OOPSLA2
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
- HORIZON EUROPE European Research Council
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 139Total Downloads
- Downloads (Last 12 months)139
- Downloads (Last 6 weeks)139
Reflects downloads up to 13 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in