research-article

From ML to ML^F: graphic type constraints with efficient type inference

Authors:

Boris YakobowskiAuthors Info & Claims

ACM SIGPLAN Notices, Volume 43, Issue 9

Pages 63 - 74

https://doi.org/10.1145/1411203.1411216

Published: 20 September 2008 Publication History

Abstract

ML^F 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 ML^F. We show that this constraint system is a small extension of the formalism of graphic types, originally introduced to represent ML^F 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 ML^F type inference, and argue that, as for ML, this complexity is linear under reasonable assumptions.

Supplementary Material

JPG File (1411216.jpg)

Download
14.10 KB

index.html (index.html)

Slides from the presentation

Download
.95 KB

ZIP File (p63-slides.zip)

Supplemental material for: From ML to MLF: graphic type constraints with efficient type inference

Download
15.54 MB

Audio only (1411216.mp3)

Download
9.08 MB

Video (1411216.mp4)

Download
125.22 MB

References

[1]

Fritz Henglein. Type inference with polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15(2):253--289, 1993.

Digital Library

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

Digital Library

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

Digital Library

[5]

Daan Leijen. Flexible types: robust type inference for first-class polymorphism. Technical Report MSR-TR-2008-55, Microsoft Research, March 2008.

Digital Library

[6]

Daan Leijen. HMF: Simple type inference for first-class polymorphism. In ICFP'08 {15}.

Digital Library

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

Digital Library

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

Digital Library

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

Digital Library

[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

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
Cui CJiang SOliveira B(2023)Greedy Implicit Bounded QuantificationProceedings of the ACM on Programming Languages10.1145/36228717:OOPSLA2(2083-2111)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622871
Show More Cited By

Index Terms

From ML to ML^F: graphic type constraints with efficient type inference
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Constraints
        Polymorphism
      2. Language types
        Functional languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

MLF: raising ML to the power of system F
Supplemental issue

We propose a type system MLF that generalizes ML with first-class polymorphism as in System F. Expressions may contain secondorder type annotations. Every typable expression admits a principal type, which however depends on type annotations. Principal ...
From ML to ML^F: graphic type constraints with efficient type inference
ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programming

ML^F 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 ML^F. We show that this constraint system is a ...
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 ...

Comments

Information & Contributors

Information

Published In

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

ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programming
September 2008
422 pages
ISBN:9781595939197
DOI:10.1145/1411204
General Chair:
James Hook
Portland State University, USA
,
Program Chair:
Peter Thiemann
Universität Freiburg, Germany

Copyright © 2008 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: 20 September 2008

Published in SIGPLAN Volume 43, Issue 9

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
271
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

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
Cui CJiang SOliveira B(2023)Greedy Implicit Bounded QuantificationProceedings of the ACM on Programming Languages10.1145/36228717:OOPSLA2(2083-2111)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622871
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
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
Friggstad ZKhodamoradi KRezapour MSalavatipour M(2019)Approximation Schemes for Clustering with OutliersACM Transactions on Algorithms10.1145/330144615:2(1-26)Online publication date: 18-Feb-2019
https://dl.acm.org/doi/10.1145/3301446
Hermelin DMnich MLeeuwen EWoeginger G(2019)Domination When the Stars Are OutACM Transactions on Algorithms10.1145/330144515:2(1-90)Online publication date: 22-Apr-2019
https://dl.acm.org/doi/10.1145/3301445
Ferraioli DVentre C(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
https://dl.acm.org/doi/10.1145/3301315
Bansal NEliéš MJeż ŁKoumoutsos G(2019)The (h,k)-Server Problem on Bounded Depth TreesACM Transactions on Algorithms10.1145/330131415:2(1-26)Online publication date: 6-Feb-2019
https://dl.acm.org/doi/10.1145/3301314
Mäkinen VTomescu AKuosmanen APaavilainen TGagie TChikhi R(2019)Sparse Dynamic Programming on DAGs with Small WidthACM Transactions on Algorithms10.1145/330131215:2(1-21)Online publication date: 6-Feb-2019
https://dl.acm.org/doi/10.1145/3301312
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.

Figures

Tables

Media

View Issue’s Table of Contents