research-article

Type inference in context

Authors:

James McKinnaAuthors Info & Claims

MSFP '10: Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming

Pages 43 - 54

https://doi.org/10.1145/1863597.1863608

Published: 25 September 2010 Publication History

Abstract

We consider the problems of first-order unification and type inference from a general perspective on problem-solving, namely that of information increase in the problem context. This leads to a powerful technique for implementing type inference algorithms. We describe a unification algorithm and illustrate the technique for the familiar Hindley-Milner type system, but it can be applied to more advanced type systems. The algorithms depend on well-founded contexts: type variable bindings and type-schemes for terms may depend only on earlier bindings. We ensure that unification yields a most general unifier, and that type inference yields principal types, by advancing definitions earlier in the context only when necessary.

References

[1]

}}F. Baader and W. Snyder. Unification theory. In J. A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, pages 445--532. Elsevier and MIT Press, 2001.

[2]

}}F. Bellegarde and J. Hook. Substitution: a formal methods case study using monads and transformations. Sci. Comp. Programming, 23(2--3):287--311, 1994.

Digital Library

[3]

}}R. Bird and R. Paterson. de Bruijn notation as a nested datatype. J. Functional Programming, 9(1):77--91, 1999.

Digital Library

[4]

}}D. Clément, T. Despeyroux, G. Kahn, and J. Despeyroux. A simple applicative language: mini-ML. In Proc. LISP and Functional Programming, pages 13--27. ACM, 1986.

Digital Library

[5]

}}L. Damas and R. Milner. Principal type-schemes for functional programs. In Proc. POPL '82, pages 207--212. ACM, 1982.

Digital Library

[6]

}}J. Dunfield. Greedy bidirectional polymorphism. In Proc. ML '09, pages 15--26. ACM, 2009.

Digital Library

[7]

}}GHC Team. The GHC user's guide, version 6.12.1. Section 7.5. Extensions to the "deriving" mechanism, 2009.

[8]

}}G. Huet. The Zipper. J. Functional Programming, 7(5):549--554, 1997.

Digital Library

[9]

}}B. J. McAdam. On the unification of substitutions in type inference. In Proc. IFL' 98, pages 139--154. Springer, 1998.

[10]

}}C. McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999.

[11]

}}C. McBride. First-Order Unification by Structural Recursion. J. Functional Programming, 13(6), 2003.

Digital Library

[12]

}}C. McBride and J. McKinna. The view from the left. J. Functional Programming, 14(1):69--111, 2004a.

Digital Library

[13]

}}C. McBride and J. McKinna. Functional pearl: I am not a number - I am a free variable. In Proc. Haskell workshop, pages 1--9. ACM, 2004b.

Digital Library

[14]

}}D. Miller. Unification under a mixed prefix. J. Symbolic Computation, 14(4):321--358, 1992.

Digital Library

[15]

}}R. Milner. A theory of type polymorphism in programming. J. Computer and System Sciences, 17(3):348--375, 1978.

[16]

}}W. Naraschewski and T. Nipkow. Type inference verified: Algorithm W in Isabelle/HOL. J. Automated Reasoning, 23(3):299--318, 1999.

Digital Library

[17]

}}T. Nipkow and C. Prehofer. Type reconstruction for type classes. J. Functional Programming, 5(2):201--224, 1995.

[18]

}}U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007.

[19]

}}R. Pollack. Implicit syntax. In Informal Proceedings of First Workshop on Logical Frameworks, 1990.

[20]

}}J. A. Robinson. A machine-oriented logic based on the resolution principle. JACM, 12(1):23--41, 1965.

Digital Library

[21]

}}J. B. Wells. The essence of principal typings. In Proc. ICALP '02, pages 913--925. Springer, 2002.

Digital Library

Cited By

Carnier DPottier FKeuchel S(2024)Type Inference LogicsProceedings of the ACM on Programming Languages10.1145/36897868:OOPSLA2(2125-2155)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689786
Dunfield JKrishnaswami N(2021)Bidirectional TypingACM Computing Surveys10.1145/345095254:5(1-38)Online publication date: 25-May-2021
https://dl.acm.org/doi/10.1145/3450952
CONVENT LLINDLEY SMCBRIDE CMCLAUGHLIN C(2020)Doo bee doo bee dooJournal of Functional Programming10.1017/S095679682000003930Online publication date: 31-Mar-2020
https://doi.org/10.1017/S0956796820000039
Show More Cited By

Index Terms

Type inference in context
1. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

ML^F for everyone (users, implementers, and designers)
ML '07: Proceedings of the 2007 workshop on Workshop on ML

ML^F is an alternative to ML that permits second-order polymorphism as in System F but retains (partial) type inference a la ML. Type annotations are requested only on parameters of functions that are used polymorphically. Type abstractions and type ...
Gradual typing with unification-based inference
DLS '08: Proceedings of the 2008 symposium on Dynamic languages

Static and dynamic type systems have well-known strengths and weaknesses. Gradual typing provides the benefits of both in a single language by giving the programmer control over which portions of the program are statically checked based on the presence ...
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94

This 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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

MSFP '10: Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming

September 2010

62 pages

ISBN:9781450302555

DOI:10.1145/1863597

General Chairs:
Venanzio Capretta
University of Nottingham, UK
,
James Chapman
Institute of Cybernetics, Tallinn, Estonia

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 September 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP '10

Sponsor:

SIGPLAN

ICFP '10: ACM SIGPLAN International Conference on Functional Programming

September 25, 2010

Maryland, Baltimore, USA

Acceptance Rates

MSFP '10 Paper Acceptance Rate 4 of 8 submissions, 50%;

Overall Acceptance Rate 4 of 8 submissions, 50%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

20
Total Citations
View Citations
246
Total Downloads

Downloads (Last 12 months)13
Downloads (Last 6 weeks)2

Reflects downloads up to 30 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Carnier DPottier FKeuchel S(2024)Type Inference LogicsProceedings of the ACM on Programming Languages10.1145/36897868:OOPSLA2(2125-2155)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689786
Dunfield JKrishnaswami N(2021)Bidirectional TypingACM Computing Surveys10.1145/345095254:5(1-38)Online publication date: 25-May-2021
https://dl.acm.org/doi/10.1145/3450952
CONVENT LLINDLEY SMCBRIDE CMCLAUGHLIN C(2020)Doo bee doo bee dooJournal of Functional Programming10.1017/S095679682000003930Online publication date: 31-Mar-2020
https://doi.org/10.1017/S0956796820000039
Xie NEisenberg ROliveira B(2019)Kind inference for datatypesProceedings of the ACM on Programming Languages10.1145/33711214:POPL(1-28)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371121
Zhao JOliveira BSchrijvers T(2019)A mechanical formalization of higher-ranked polymorphic type inferenceProceedings of the ACM on Programming Languages10.1145/33417163:ICFP(1-29)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341716
Zhao JC. d. S. Oliveira BSchrijvers T(2018)Formalization of a Polymorphic Subtyping AlgorithmInteractive Theorem Proving10.1007/978-3-319-94821-8_36(604-622)Online publication date: 4-Jul-2018
https://doi.org/10.1007/978-3-319-94821-8_36
Lindley SMcBride CMcLaughlin C(2017)Do be do be doACM SIGPLAN Notices10.1145/3093333.300989752:1(500-514)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009897
Azevedo de Amorim AGaboardi MHsu JKatsumata SCherigui I(2017)A semantic account of metric preservationACM SIGPLAN Notices10.1145/3093333.300989052:1(545-556)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009890
Ahman DHriţcu CMaillard KMartínez GPlotkin GProtzenko JRastogi ASwamy N(2017)Dijkstra monads for freeACM SIGPLAN Notices10.1145/3093333.300987852:1(515-529)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009878
Kopczyński EToruńczyk S(2017)LOIS: syntax and semanticsACM SIGPLAN Notices10.1145/3093333.300987652:1(586-598)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009876
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents