research-article

Flexible types: robust type inference for first-class polymorphism

Author:

Daan LeijenAuthors Info & Claims

ACM SIGPLAN Notices, Volume 44, Issue 1

Pages 66 - 77

https://doi.org/10.1145/1594834.1480891

Published: 21 January 2009 Publication History

Abstract

We present HML, a type inference system that supports full first-class polymorphism where few annotations are needed: only function parameters with a polymorphic type need to be annotated. HML is a simplification of MLF where only flexibly quantified types are used. This makes the types easier to work with from a programmers perspective, and simplifies the implementation of the type inference algorithm. Still, HML retains much of the expressiveness of MLF, it is robust with respect to small program transformations, and has a simple specification of the type rules with an effective type inference algorithm that infers principal types. A small reference implementation with many examples is available at: http://research.microsoft.com/users/daan/pubs.html.

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.

Digital Library

[4]

Atze Dijkstra. Stepping through Haskell. PhD thesis, Universiteit Utrecht, Nov. 2005.

[5]

Jacques Garrigue and Didier R´emy. Semi-explicit first-class polymorphism for ML. Journal of Information and Computation, 155:134--169, 1999.

Digital Library

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

Digital Library

[8]

George Kuan and David MacQueen. Efficient ML type inference using ranked type variables. In The 2007 ACM SIGPLAN Workshop on ML (ML 2007), Freiburg, Germany, October 2007.

Digital Library

[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´emy. MLF: Raising ML to the power of System-F. In The International Conference on Functional Programming (ICFP'03), pages 27--38, aug 2003.

Digital Library

[11]

Didier Le Botlan and Didier R´emy. Recasting MLF. Research Report 6228, INRIA, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, June 2007.

[12]

Daan Leijen. HMF: Simple type inference for first-class polymorphism. In 13th ACM symp. of the International Conference on Functional Programming (ICFP'08), September 2008a. Extended version available as a technical report: MSR-TR-2007-118, Sep 2007, Microsoft Research.

Digital Library

[13]

Daan Leijen. A reference implementation of HML. Available at http://research.microsoft.com/users/daan/pubs. html, April 2008b.

[14]

Daan Leijen. A type directed translation from MLF to System F. In The International Conference on Functional Programming (ICFP'07), Oct. 2007.

Digital Library

[15]

Daan Leijen and Andres Löh. Qualified types for MLF. In The International Conference on Functional Programming (ICFP'05). ACM Press, Sep. 2005.

Digital Library

[16]

Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:248--375, 1978.

[17]

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.

Digital Library

[18]

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.

Digital Library

[19]

Didier R´emy. Simple, partial type-inference for System-F based on type-containment. In The International Conference on Functional Programming (ICFP'05), September 2005.

Digital Library

[20]

Didier R´emy and Boris Yakobowski. A graphical presentation of MLF types with a linear-time unification algorithm. In TLDI'07, pages 27--38, 2007.

Digital Library

[21]

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.

Digital Library

[22]

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.

Digital Library

[23]

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

Xie NBi XOliveira BSchrijvers T(2019)Consistent Subtyping for AllACM Transactions on Programming Languages and Systems10.1145/331033942:1(1-79)Online publication date: 21-Nov-2019
https://dl.acm.org/doi/10.1145/3310339
Serrano AHage JVytiniotis DPeyton Jones S(2018)Guarded impredicative polymorphismACM SIGPLAN Notices10.1145/3296979.319238953:4(783-796)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192389
Serrano AHage JVytiniotis DPeyton Jones SFoster JGrossman D(2018)Guarded impredicative polymorphismProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192389(783-796)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192389
Show More Cited By

Index Terms

Flexible types: robust type inference for first-class polymorphism
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Polymorphism

Recommendations

Flexible types: robust type inference for first-class polymorphism
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We present HML, a type inference system that supports full first-class polymorphism where few annotations are needed: only function parameters with a polymorphic type need to be annotated. HML is a simplification of MLF where only flexibly quantified ...
A type directed translation of MLF to system F
Proceedings of the ICFP '07 conference

The MLF type system by Le Botlan and Rémy is a natural extension of Hindley-Milner type inference that supports full first-class polymorphism, where types can be of higher-rank and impredicatively instantiated. Even though MLF is theoretically very ...
A type directed translation of MLF to system F
ICFP '07: Proceedings of the 12th ACM SIGPLAN international conference on Functional programming

The MLF type system by Le Botlan and Rémy is a natural extension of Hindley-Milner type inference that supports full first-class polymorphism, where types can be of higher-rank and impredicatively instantiated. Even though MLF is theoretically very ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 44, Issue 1

POPL '09

January 2009

453 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1594834

Issue’s Table of Contents

POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2009
464 pages
ISBN:9781605583792
DOI:10.1145/1480881
General Chair:
Zhong Shao
Yale University, USA
,
Program Chair:
Benjamin C. Pierce
University of Pennsylvania, USA

Copyright © 2009 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 January 2009

Published in SIGPLAN Volume 44, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
416
Total Downloads

Downloads (Last 12 months)16
Downloads (Last 6 weeks)5

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Xie NBi XOliveira BSchrijvers T(2019)Consistent Subtyping for AllACM Transactions on Programming Languages and Systems10.1145/331033942:1(1-79)Online publication date: 21-Nov-2019
https://dl.acm.org/doi/10.1145/3310339
Serrano AHage JVytiniotis DPeyton Jones S(2018)Guarded impredicative polymorphismACM SIGPLAN Notices10.1145/3296979.319238953:4(783-796)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192389
Serrano AHage JVytiniotis DPeyton Jones SFoster JGrossman D(2018)Guarded impredicative polymorphismProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192389(783-796)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192389
Xie NOliveira B(2018)Let Arguments Go FirstProgramming Languages and Systems10.1007/978-3-319-89884-1_10(272-299)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89884-1_10
Leijen DLindley SYorgey B(2017)Structured asynchrony with algebraic effectsProceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3122975.3122977(16-29)Online publication date: 3-Sep-2017
https://dl.acm.org/doi/10.1145/3122975.3122977
Lenglet SWells J(2012)Expansion for universal quantifiersProceedings of the 21st European conference on Programming Languages and Systems10.1007/978-3-642-28869-2_23(456-475)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28869-2_23
Botlan DRémy D(2009)Recasting MLFInformation and Computation10.1016/j.ic.2008.12.006207:6(726-785)Online publication date: 1-Jun-2009
https://dl.acm.org/doi/10.1016/j.ic.2008.12.006
Parreaux LBoruch-Gruszecki AFan AChau C(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
https://dl.acm.org/doi/10.1145/3632890
Kovács A(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
https://dl.acm.org/doi/10.1145/3408983
Serrano AHage JPeyton Jones SVytiniotis D(2020)A quick look at impredicativityProceedings of the ACM on Programming Languages10.1145/34089714:ICFP(1-29)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408971
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 Issue’s Table of Contents