skip to main content
10.1145/2676726.2676991acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction

Published: 14 January 2015 Publication History

Abstract

This article is the second part of a two articles series about the definition of higher order polymorphic functions in a type system with recursive types and set-theoretic type connectives (unions, intersections, and negations).
In the first part, presented in a companion paper, we defined and studied the syntax, semantics, and evaluation of the explicitly-typed version of a calculus, in which type instantiation is driven by explicit instantiation annotations. In this second part we present a local type inference system that allows the programmer to omit explicit instantiation annotations for function applications, and a type reconstruction system that allows the programmer to omit explicit type annotations for function definitions.
The work presented in the two articles provides the theoretical foundations and technical machinery needed to design and implement higher-order polymorphic functional languages with union and intersection types and/or for semi-structured data processing.

Supplementary Material

ZIP File (popl153.zip)
Appendix of the article "Polymorphic Functions with Set-Theoretic Types (Part 2: Local Type Inference and Type Reconstruction)"
MPG File (p289-sidebyside.mpg)

References

[1]
A. Aiken and E. L. Wimmers. Type inclusion constraints and type inference. In FPCA'93, pages 31--41, 1993.
[2]
V. Benzaken, G. Castagna, and A. Frisch. CDuce: an XML-friendly general purpose language. In ICFP'03. ACM Press, 2003.
[3]
G. Castagna, K. Nguyen, Z. Xu, H. Im, S. Lenglet, and L. Padovani. Polymorphic functions with set-theoretic types. Part 1: Syntax, semantics, and evaluation. In POPL'14, January 2014.
[4]
G. Castagna and Z. Xu. Set-theoretic Foundation of Parametric Poly- morphism and Subtyping. In ICFP'11, 2011.
[5]
B. Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25:95--169, 1983.
[6]
L. Damas and R. Milner. Principal type-schemes for functional programs. In POPL'82, pages 207--212, 1982.
[7]
R. Davies. Practical Refiniment-Type Checking. PhD thesis, Carnegie Mellon University, 2005.
[8]
J. Robie et al. XQuery 3.0: An XML query language (working draft 2010/12/14), 2010. http://www.w3.org/TR/xquery-30/.
[9]
A. Frisch. Théorie, conception et réalisation dun langage de programmation fonctionnel adapté à XML. PhD thesis, U. Paris 7, 2004.
[10]
A. Frisch, G. Castagna, and V. Benzaken. Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types. The Journal of ACM, 55(4):1--64, 2008.
[11]
A. Martelli and U. Montanari. An efficient unification algorithm. ACM TOPLAS, 4(2):258--282, 1982.
[12]
M. Odersky, M. Sulzmann, and M. Wehr. Type inference with constrained types. TAPOS, 5(1):35--55, 1999.
[13]
C. Okasaki. Purely Functional Data Structures. CUP, 1998.
[14]
B.C. Pierce and D.N. Turner. Local type inference. ACM Trans. Program. Lang. Syst., 22(1):1--44, 2000.
[15]
F. Pottier and D. Rémy. The essence of ML type inference. In B.C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10, pages 389--489. MIT Press, 2005.
[16]
S. Tobin-Hochstadt and M. Felleisen. The design and implementation of typed scheme. In POPL'08, 2008.
[17]
S. Tobin-Hochstadt and M. Felleisen. Logical types for untyped languages. In ICFP'10, 2010.
[18]
Z. Xu. Parametric Polymorphism for XML Processing Languages. PhD thesis, Université Paris Diderot, 2013. Available at http://tel.archives-ouvertes.fr/tel-00858744

Cited By

View all
  • (2024)The Ultimate Conditional SyntaxProceedings of the ACM on Programming Languages10.1145/36897468:OOPSLA2(988-1017)Online publication date: 8-Oct-2024
  • (2024)Same Same but Different: A Comparative Analysis of Static Type Checkers in ErlangProceedings of the 23rd ACM SIGPLAN International Workshop on Erlang10.1145/3677995.3678189(2-12)Online publication date: 28-Aug-2024
  • (2024)Decidable Subtyping of Existential Types for JuliaProceedings of the ACM on Programming Languages10.1145/36564218:PLDI(1091-1114)Online publication date: 20-Jun-2024
  • Show More Cited By

Index Terms

  1. Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction

    Recommendations

    Comments

    Information & Contributors

    Information

    Published In

    cover image ACM Conferences
    POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
    January 2015
    716 pages
    ISBN:9781450333009
    DOI:10.1145/2676726
    • cover image ACM SIGPLAN Notices
      ACM SIGPLAN Notices  Volume 50, Issue 1
      POPL '15
      January 2015
      682 pages
      ISSN:0362-1340
      EISSN:1558-1160
      DOI:10.1145/2775051
      • Editor:
      • Andy Gill
      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 the author(s) 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

    In-Cooperation

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    Published: 14 January 2015

    Permissions

    Request permissions for this article.

    Check for updates

    Author Tags

    1. intersection types
    2. polymorphism
    3. semantic subtyping
    4. type constraints
    5. types
    6. xml

    Qualifiers

    • Research-article

    Funding Sources

    Conference

    POPL '15
    Sponsor:

    Acceptance Rates

    POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;
    Overall Acceptance Rate 860 of 4,328 submissions, 20%

    Upcoming Conference

    POPL '26

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)19
    • Downloads (Last 6 weeks)5
    Reflects downloads up to 19 Feb 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2024)The Ultimate Conditional SyntaxProceedings of the ACM on Programming Languages10.1145/36897468:OOPSLA2(988-1017)Online publication date: 8-Oct-2024
    • (2024)Same Same but Different: A Comparative Analysis of Static Type Checkers in ErlangProceedings of the 23rd ACM SIGPLAN International Workshop on Erlang10.1145/3677995.3678189(2-12)Online publication date: 28-Aug-2024
    • (2024)Decidable Subtyping of Existential Types for JuliaProceedings of the ACM on Programming Languages10.1145/36564218:PLDI(1091-1114)Online publication date: 20-Jun-2024
    • (2024)Polymorphic Type Inference for Dynamic LanguagesProceedings of the ACM on Programming Languages10.1145/36328828:POPL(1179-1210)Online publication date: 5-Jan-2024
    • (2023)Typing Records, Maps, and StructsProceedings of the ACM on Programming Languages10.1145/36078387:ICFP(215-258)Online publication date: 31-Aug-2023
    • (2023)Making a Type Difference: Subtraction on Intersection Types as Generalized Record OperationsProceedings of the ACM on Programming Languages10.1145/35712247:POPL(893-920)Online publication date: 11-Jan-2023
    • (2023)Programming with Union, Intersection, and Negation TypesThe French School of Programming10.1007/978-3-031-34518-0_12(309-378)Online publication date: 11-Oct-2023
    • (2022)Set-theoretic Types for ErlangProceedings of the 34th Symposium on Implementation and Application of Functional Languages10.1145/3587216.3587220(1-14)Online publication date: 31-Aug-2022
    • (2022)On type-cases, union elimination, and occurrence typingProceedings of the ACM on Programming Languages10.1145/34986746:POPL(1-31)Online publication date: 12-Jan-2022
    • (2022)Revisiting occurrence typingScience of Computer Programming10.1016/j.scico.2022.102781217:COnline publication date: 1-May-2022
    • 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