skip to main content
10.1145/1411204.1411245acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
research-article

HMF: simple type inference for first-class polymorphism

Published: 20 September 2008 Publication History

Abstract

HMF is a conservative extension of Hindley-Milner type inference with first-class polymorphism. In contrast to other proposals, HML uses regular System F types and has a simple type inference algorithm that is just a small extension of the usual Damas-Milner algorithm W. Given the relative simplicity and expressive power, we feel that HMF can be an attractive type system in practice. There is a reference implementation of the type system available online together with a technical report containing proofs (Leijen 2007a,b).

Supplementary Material

JPG File (1411245.jpg)
index.html (index.html)
Slides from the presentation
ZIP File (p283-slides.zip)
Supplemental material for: HMF: simple type inference for first-class polymorphism
Audio only (1411245.mp3)
Video (1411245.mp4)

References

[1]
H. Curry and R. Feys. Combinatory Logic, volume 1. North-Holland, 1958.
[2]
Luis Damas. Type Assignment in Programming Languages. PhD thesis, University of Edinburgh, April 1985. Technical report CST-33-85.
[3]
Luis Damas and Robin Milner. Principal type-schemes for functional programs. In 9th ACM symp. on Principles of Programming Languages (POPL'82), pages 207--212, 1982.
[4]
Atze Dijkstra. Stepping through Haskell. PhD thesis, Universiteit Utrecht, Nov. 2005.
[5]
Jacques Garrigue and Didier Rémy. Semi-explicit first-class polymorphism for ML. Journal of Information and Computation, 155:134--169, 1999.
[6]
J.R. Hindley. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29--60, Dec. 1969.
[7]
Mark P. Jones. First-class polymorphism with type inference. In 24th ACM Symposium on Principles of Programming Languages (POPL'97), January 1997.
[8]
Mark P. Jones. Formal properties of the Hindley-Milner type system. Unpublished notes, August 1995.
[9]
Didier Le Botlan. MLF: Une extension de ML avec polymorphisme de second ordre et instanciation implicite. PhD thesis, INRIA Rocquencourt, May 2004. Also in English.
[10]
Didier Le Botlan and Didier Rémy. MLF: Raising ML to the power of System-F. In The International Conference on Functional Programming (ICFP'03), pages 27--38, aug 2003.
[11]
Didier Le Botlan and Didier Rémy. Recasting MLF. Research Report 6228, INRIA, Rocquencourt, France, June 2007.
[12]
Daan Leijen. A reference implementation of HMF. Available at http://research.microsoft.com/users/daan/pubs.html, September 2007a.
[13]
Daan Leijen. HMF: Simple type inference for first-class polymorphism. Technical Report MSR-TR-2007-118, Microsoft Research, September 2007b. Extended version with proofs.
[14]
Daan Leijen. Flexible types: robust type inference for first-class polymorphism. Technical Report MSR-TR-2008-55, Microsoft Research, March 2008.
[15]
Daan Leijen. A type directed translation from MLF to System F. In The International Conference on Functional Programming (ICFP'07), Oct. 2007c.
[16]
Daan Leijen and Andres Löh. Qualified types for MLF. In The International Conference on Functional Programming (ICFP'05). ACM Press, Sep. 2005.
[17]
Xavier Leroy and M Mauny. Dynamics in ML. In ACM conference on Functional Programming and Computer Architecture (FPCA'91). Springer-Verlag, 1991. volume 523 of LNCS.
[18]
Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:248--375, 1978.
[19]
Martin Odersky and Konstantin Läufer. Putting type annotations to work. In 23th ACM symp. on Principles of Programming Languages (POPL'96), pages 54--67, January 1996.
[20]
Simon Peyton Jones and Mark Shields. Lexically scoped type variables. Draft, March 2004.
[21]
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.
[22]
Benjamin C. Pierce and David N. Turner. Local type inference. In 25th ACM symp. on Principles of Programming Languages (POPL'98), pages 252--265, 1998.
[23]
Didier Rémy. Simple, partial type-inference for System-F based on type-containment. In The International Conference on Functional Programming (ICFP'05), September 2005.
[24]
Didier Rémy and Boris Yakobowski. A graphical presentation of MLF types with a linear-time unification algorithm. In TLDI'07, pages 27--38, 2007.
[25]
J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23--41, January 1965.
[26]
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. Boxy types: type inference for higher-rank types and impredicativity. In The International Conference on Functional Programming (ICFP'06), September 2006.
[27]
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. FPH : First-class polymorphism for Haskell. In 13th ACM symp. of the International Conference on Functional Programming (ICFP'08), September 2008.
[28]
J.B.Wells. Typability and type checking in System-F are equivalent and undecidable. Ann. Pure Appl. Logic, 98(1-3):111--156,1999.

Cited By

View all
  • (2025)Bidirectional Higher-Rank Polymorphism with Intersection and Union TypesProceedings of the ACM on Programming Languages10.1145/37049079:POPL(2118-2148)Online publication date: 9-Jan-2025
  • (2024)Contextual TypingProceedings of the ACM on Programming Languages10.1145/36746558:ICFP(880-908)Online publication date: 15-Aug-2024
  • (2024)Soundly Handling LinearityProceedings of the ACM on Programming Languages10.1145/36328968:POPL(1600-1628)Online publication date: 5-Jan-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programming
September 2008
422 pages
ISBN:9781595939197
DOI:10.1145/1411204
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 43, Issue 9
    ICFP '08
    September 2008
    399 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/1411203
    Issue’s Table of Contents
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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 September 2008

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. first-class polymorphism
  2. type inference

Qualifiers

  • Research-article

Conference

ICFP08
Sponsor:

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25
ACM SIGPLAN International Conference on Functional Programming
October 12 - 18, 2025
Singapore , Singapore

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)35
  • Downloads (Last 6 weeks)2
Reflects downloads up to 18 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)Bidirectional Higher-Rank Polymorphism with Intersection and Union TypesProceedings of the ACM on Programming Languages10.1145/37049079:POPL(2118-2148)Online publication date: 9-Jan-2025
  • (2024)Contextual TypingProceedings of the ACM on Programming Languages10.1145/36746558:ICFP(880-908)Online publication date: 15-Aug-2024
  • (2024)Soundly Handling LinearityProceedings of the ACM on Programming Languages10.1145/36328968:POPL(1600-1628)Online publication date: 5-Jan-2024
  • (2024)When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class PolymorphismProceedings of the ACM on Programming Languages10.1145/36328908:POPL(1418-1450)Online publication date: 5-Jan-2024
  • (2023)Greedy Implicit Bounded QuantificationProceedings of the ACM on Programming Languages10.1145/36228717:OOPSLA2(2083-2111)Online publication date: 16-Oct-2023
  • (2023)Sound and Complete Type Inference for Closed Effect RowsTrends in Functional Programming10.1007/978-3-031-21314-4_8(144-168)Online publication date: 1-Jan-2023
  • (2022)First-class names for effect handlersProceedings of the ACM on Programming Languages10.1145/35632896:OOPSLA2(30-59)Online publication date: 31-Oct-2022
  • (2022)Constraint-based type inference for FreezeMLProceedings of the ACM on Programming Languages10.1145/35476426:ICFP(570-595)Online publication date: 31-Aug-2022
  • (2020)Elaboration with first-class implicit function typesProceedings of the ACM on Programming Languages10.1145/34089834:ICFP(1-29)Online publication date: 3-Aug-2020
  • (2020)A quick look at impredicativityProceedings of the ACM on Programming Languages10.1145/34089714:ICFP(1-29)Online publication date: 3-Aug-2020
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media