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

FPH: first-class polymorphism for Haskell

Published: 20 September 2008 Publication History

Abstract

Languages supporting polymorphism typically have ad-hoc restrictions on where polymorphic types may occur. Supporting "firstclass" polymorphism, by lifting those restrictions, is obviously desirable, but it is hard to achieve this without sacrificing type inference. We present a new type system for higher-rank and impredicative polymorphism that improves on earlier proposals: it is an extension of Damas-Milner; it relies only on System F types; it has a simple, declarative specification; it is robust to program transformations; and it enjoys a complete and decidable type inference algorithm.

Supplementary Material

JPG File (1411246.jpg)
index.html (index.html)
Slides from the presentation
ZIP File (p295-slides.zip)
Supplemental material for: FPH: first-class polymorphism for Haskell
Audio only (1411246.mp3)
Video (1411246.mp4)

References

[1]
Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Conference Record of the 9th Annual ACM Symposium on Principles of Programming Languages, pages 207--12, New York, 1982. ACM Press.
[2]
Jacques Garrigue and Didier Rémy. Semi-explicit first-class polymorphism for ML. Journal of Information and Computation, 155:134--169, 1999.
[3]
AJ Kfoury and JB Wells. A direct algorithm for type inference in the rank-2 fragment of the second-order lambda calculus. In ACM Symposium on Lisp and Functional Programming, pages 196--207. ACM, Orlando, Florida, June 1994.
[4]
D Le Botlan and D Rémy. MLF: raising ML to the power of System F. In ACM SIGPLAN International Conference on Functional Programming (ICFP'03), pages 27--38, Uppsala, Sweden, September 2003. ACM.
[5]
Didier Le Botlan. MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite. PhD thesis, Ecole Polytechnique, May 2004. 326 pages, also available in english.
[6]
Didier Le Botlan and Didier Rémy. Recasting MLF. Research Report 6228, INRIA, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, June 2007.
[7]
Daan Leijen. HMF: simple type inference for first-class polymorphism. In ACM SIGPLAN International Conference on Functional Programming (ICFP'08). ACM, 2008a.
[8]
Daan Leijen. Flexible types: robust type inference for first-class polymorphism. Technical Report MSR-TR-2008-55, Microsoft Research, March 2008b.
[9]
Daan Leijen. A type directed translation of MLF to System-F. In ACM SIGPLAN International Conference on Functional Programming (ICFP'07), Freiburg, Germany, 2007. ACM.
[10]
Daan Leijen and Andres Löh. Qualified types for MLF. In ACM SIGPLAN International Conference on Functional Programming (ICFP'06), pages 144--155. ACM Press, 2005.
[11]
R Milner. A theory of type polymorphism in programming. JCSS, 13(3), December 1978.
[12]
John C. Mitchell. Polymorphic type inference and containment. Inf. Comput., 76(2-3):211--249, 1988. ISSN 0890-5401.
[13]
M Odersky and K Läufer. Putting type annotations to work. In 23rd ACM Symposium on Principles of Programming Languages (POPL'96), pages 54--67. ACM, St Petersburg Beach, Florida, January 1996.
[14]
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical type inference for arbitrary-rank types. J. Funct. Program., 17(1):1--82, 2007. ISSN 0956-7968.
[15]
Frank Pfenning. Partial polymorphic type inference and higher-order unification. In LFP '88: Proceedings of the 1988 ACM conference on LISP and functional programming, pages 153--163, New York, NY, USA, 1988. ACM. ISBN 0-89791-273-X.
[16]
Didier Rémy. Simple, partial type inference for System F, based on type containment. In ACM SIGPLAN International Conference on Functional Programming (ICFP'05), pages 130--143, Tallinn, Estonia, September 2005. ACM.
[17]
Dimitrios Vytiniotis. Practical type inference for first-class polymorphism. PhD thesis, University of Pennsylvania, 2008. URL www.cis.upenn.edu/~dimitriv/fph. In submission.
[18]
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. Boxy types: Inference for higher-rank types and impredicativity. In ACM SIGPLAN International Conference on Functional Programming (ICFP'06), Portland, Oregon, 2006. ACM Press.
[19]
JB Wells. Typability and type checking in system F are equivalent and undecidable. Ann. Pure Appl. Logic, 98: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)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
  • 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. higher-rank types
  2. impredicativity
  3. 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)3
  • Downloads (Last 6 weeks)1
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)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
  • (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
  • (2020)FreezeML: complete and easy type inference for first-class polymorphismProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3386003(423-437)Online publication date: 11-Jun-2020
  • (2019)Kind inference for datatypesProceedings of the ACM on Programming Languages10.1145/33711214:POPL(1-28)Online publication date: 20-Dec-2019
  • (2019)Lambda: the ultimate sublanguage (experience report)Proceedings of the ACM on Programming Languages10.1145/33427133:ICFP(1-17)Online publication date: 26-Jul-2019
  • (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
  • (2019)Consistent Subtyping for AllACM Transactions on Programming Languages and Systems10.1145/331033942:1(1-79)Online publication date: 21-Nov-2019
  • 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