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

From ML to MLF: graphic type constraints with efficient type inference

Published: 20 September 2008 Publication History

Abstract

MLF is a type system that seamlessly merges ML-style type inference with System-F polymorphism. We propose a system of graphic (type) constraints that can be used to perform type inference in both ML or MLF. We show that this constraint system is a small extension of the formalism of graphic types, originally introduced to represent MLF types. We give a few semantic preserving transformations on constraints and propose a strategy for applying them to solve constraints. We show that the resulting algorithm has optimal complexity for MLF type inference, and argue that, as for ML, this complexity is linear under reasonable assumptions.

Supplementary Material

JPG File (1411216.jpg)
index.html (index.html)
Slides from the presentation
ZIP File (p63-slides.zip)
Supplemental material for: From ML to MLF: graphic type constraints with efficient type inference
Audio only (1411216.mp3)
Video (1411216.mp4)

References

[1]
Fritz Henglein. Type inference with polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15(2):253--289, 1993.
[2]
Didier Le Botlan and Didier Rémy. MLF: Raising ML to the power of System-F. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pages 27--38, August 2003.
[3]
Didier Le Botlan and Didier Rémy. Recasting MLF. Research Report 6228, INRIA, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, June 2007.
[4]
Daan Leijen. A type directed translation of MLF to system F. In Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming (ICFP'07), Freiburg, Germany, pages 111--122, October 2007.
[5]
Daan Leijen. Flexible types: robust type inference for first-class polymorphism. Technical Report MSR-TR-2008-55, Microsoft Research, March 2008.
[6]
Daan Leijen. HMF: Simple type inference for first-class polymorphism. In ICFP'08 {15}.
[7]
David McAllester. A logical algorithm for ML type inference. In International Conference on Rewriting Techniques and Applications (RTA), Valencia, Spain, volume 2706 of Lecture Notes in Computer Science, pages 436--451. Springer-Verlag, June 2003.
[8]
François Pottier and Didier Rémy. The essence of ML type inference. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10, pages 389--489. MIT Press, 2005.
[9]
Didier Rémy. Extending ML type system with a sorted equational theory. Research Report 1766, INRIA, 1992.
[10]
Didier Rémy and Boris Yakobowski. A graphical presentation of MLF types with a linear-time unification algorithm. In Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI'07), pages 27--38, Nice, France, January 2007. ACM Press.
[11]
Didier Rémy and Boris Yakobowski. A Church-style intermediate language for MLF. Submitted, available at http://gallium.inria.fr/~remy/mlf, 2008.
[12]
Didier Rémy and Boris Yakobowski. A graphical presentation of MLF types with a linear-time incremental unification algorithm. Extended version, of {10}, September 2008.
[13]
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. FPH: First-class polymorphism for Haskell. In ICFP'08 {15}.
[14]
Joe B.Wells. Typability and type checking in system F are equivalent and undecidable. Annals of Pure and Applied Logic, 98(1--3):111--156, 1999.
[15]
Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP'08), Victoria, British Columbia, Canada. ACM Press, September 2008.

Cited By

View all
  • (2023)Greedy Implicit Bounded QuantificationProceedings of the ACM on Programming Languages10.1145/36228717:OOPSLA2(2083-2111)Online publication date: 16-Oct-2023
  • (2019)Kind inference for datatypesProceedings of the ACM on Programming Languages10.1145/33711214:POPL(1-28)Online publication date: 20-Dec-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

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. ML
  2. MLF
  3. binders
  4. graphs
  5. system F
  6. type constraints
  7. type generalization
  8. type inference
  9. type instantiation
  10. types
  11. unification

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)4
  • Downloads (Last 6 weeks)0
Reflects downloads up to 18 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2023)Greedy Implicit Bounded QuantificationProceedings of the ACM on Programming Languages10.1145/36228717:OOPSLA2(2083-2111)Online publication date: 16-Oct-2023
  • (2019)Kind inference for datatypesProceedings of the ACM on Programming Languages10.1145/33711214:POPL(1-28)Online publication date: 20-Dec-2019
  • (2019)Consistent Subtyping for AllACM Transactions on Programming Languages and Systems10.1145/331033942:1(1-79)Online publication date: 21-Nov-2019
  • (2019)Approximation Schemes for Clustering with OutliersACM Transactions on Algorithms10.1145/330144615:2(1-26)Online publication date: 18-Feb-2019
  • (2019)Domination When the Stars Are OutACM Transactions on Algorithms10.1145/330144515:2(1-90)Online publication date: 22-Apr-2019
  • (2019)Metastability of the Logit Dynamics for Asymptotically Well-Behaved Potential GamesACM Transactions on Algorithms10.1145/330131515:2(1-42)Online publication date: 6-Feb-2019
  • (2019)The (h,k)-Server Problem on Bounded Depth TreesACM Transactions on Algorithms10.1145/330131415:2(1-26)Online publication date: 6-Feb-2019
  • (2019)Sparse Dynamic Programming on DAGs with Small WidthACM Transactions on Algorithms10.1145/330131215:2(1-21)Online publication date: 6-Feb-2019
  • (2018)Guarded impredicative polymorphismACM SIGPLAN Notices10.1145/3296979.319238953:4(783-796)Online publication date: 11-Jun-2018
  • (2018)Let Arguments Go FirstProgramming Languages and Systems10.1007/978-3-319-89884-1_10(272-299)Online publication date: 14-Apr-2018
  • 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