research-article

Set-theoretic foundation of parametric polymorphism and subtyping

Authors:

Giuseppe Castagna,

Zhiwu XuAuthors Info & Claims

ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming

Pages 94 - 106

https://doi.org/10.1145/2034773.2034788

Published: 19 September 2011 Publication History

Abstract

We define and study parametric polymorphism for a type system with recursive, product, union, intersection, negation, and function types. We first recall why the definition of such a system was considered hard "when not impossible" and then present the main ideas at the basis of our solution. In particular, we introduce the notion of "convexity" on which our solution is built up and discuss its connections with parametricity as defined by Reynolds to whose study our work sheds new light.

Supplementary Material

MP4 File (_talk9.mp4)

Download
58.47 MB

References

[1]

V. Balat, J. Vouillon, and B. Yakobowski. Experience report: Ocsigen, a web programming framework. In ICFP '09. ACM Press, 2009.

Digital Library

[2]

V. Benzaken, G. Castagna, and A. Frisch. CDuce: an XML-friendly general purpose language. In ICFP '03. ACM Press, 2003.

Digital Library

[3]

G. Castagna, R. De Nicola, and D. Varacca. Semantic subtyping for the π-calculus. Theor. Comput. Sci., 398(1-3):217--242, 2008.

Digital Library

[4]

G. Castagna and K. Nguyen. Typed iterators for XML. In ICFP '08, pages 15--26. ACM Press, 2008.

Digital Library

[5]

J. Clark and M. Murata. Relax-NG, 2001. www.relaxng.org.

[6]

D. Draper et al. XQuery 1.0 and XPath 2.0 Formal Semantics, 2007. http://www.w3.org/TR/query-semantics/.

[7]

T. Berners-Lee et al. Uniform Resource Identifier, January 2005. RFC 3986, STD 66.

[8]

A. Frisch. Théorie, conception et réalisation d'un langage de programmation fonctionnel adapté à XML. PhD thesis, Université Paris 7, December 2004.

[9]

A. Frisch. OCaml + XDuce. In ICFP'06. ACM Press, 2006.

Digital Library

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

Digital Library

[11]

V. Gapeyev, M.Y. Levin, B.C. Pierce, and A. Schmitt. The Xtatic compiler and runtime system, 2005. http://www.cis.upenn.edu/~bcpierce/xtatic.

[12]

J. Garrigue. Programming with polymorphic variants. In Proc. of ML Workshop, 1998.

[13]

P. Genevès, N. Layaïda, and A. Schmitt. Efficient static analysis of XML paths and types. In PLDI '07. ACM Press, 2007.

Digital Library

[14]

N. Gesbert, P. Genevès, and N. Layaïda. Parametric Polymorphism and Semantic Subtyping: the Logical Connection. In ICFP '11, 2011.

Digital Library

[15]

H. Hosoya, A. Frisch, and G. Castagna. Parametric polymorphism for XML. ACM TOPLAS, 32(1):1--56, 2009.

Digital Library

[16]

H. Hosoya and B. Pierce. XDuce: A statically typed XML processing language. ACM TOIT, 3(2):117--148, 2003.

Digital Library

[17]

K. Zhuo Ming Lu and M. Sulzmann. An implementation of subtyping among regular expression types. In Proc. of APLAS '04, volume 3302 of LNCS, pages 57--73. Springer, 2004.

[18]

J. C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing, pages 513--523. Elsevier, 1983.

[19]

J. C. Reynolds. Polymorphism is not set-theoretic. In Semantics of Data Types, volume 173 of LNCS, pages 145--156. Springer, 1984.

[20]

J. Vouillon. Polymorphic regular tree types and patterns. In POPL'06, pages 103--114, 2006.

Digital Library

[21]

W3C. SOAP Version 1.2. http://www.w3.org/TR/soap.

[22]

P. Wadler. Theorems for free! In Functional Programming Languages and Computer Architecture, pages 347--359. ACM Press, 1989.

Digital Library

[23]

C. Wallace and C. Runciman. Haskell and XML: Generic combinators or type based translation? In ICFP '99, pages 148--159, 1999.

Digital Library

[24]

H. Xi, C. Chen, and G. Chen. Guarded recursive datatype constructors. In POPL'03, pages 224--235. ACM Press, 2003.

Digital Library

Cited By

Berger FSchimpf ABieniusa AWehr SFernandez-Reyes KVoinea A(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
https://dl.acm.org/doi/10.1145/3677995.3678189
Castagna GLaurent MNguyễn K(2024)Polymorphic Type Inference for Dynamic LanguagesProceedings of the ACM on Programming Languages10.1145/36328828:POPL(1179-1210)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632882
Castagna G(2023)Typing Records, Maps, and StructsProceedings of the ACM on Programming Languages10.1145/36078387:ICFP(215-258)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607838
Show More Cited By

Index Terms

Set-theoretic foundation of parametric polymorphism and subtyping
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
        Polymorphism
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

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, ...
Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

This article is the first part of a two articles series about a calculus with higher-order polymorphic functions, recursive types with arrow and product type constructors and set-theoretic type connectives (union, intersection, and negation).

In this ...
Set-theoretic foundation of parametric polymorphism and subtyping
ICFP '11

We define and study parametric polymorphism for a type system with recursive, product, union, intersection, negation, and function types. We first recall why the definition of such a system was considered hard "when not impossible" and then present the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming

September 2011

470 pages

ISBN:9781450308656

DOI:10.1145/2034773

General Chairs:
Manuel Chakravarty
University of New South Wales, Australia
,
Zhenjiang Hu
National Institute of Informatics, Japan
,
Program Chair:
Olivier Danvy
Aarhus University, Denmark

ACM SIGPLAN Notices Volume 46, Issue 9
ICFP '11
September 2011
456 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2034574
Issue’s Table of Contents

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

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 September 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP '11

Sponsor:

SIGPLAN

ICFP '11: ACM SIGPLAN International Conference on Functional Programming

September 19 - 21, 2011

Tokyo, Japan

Acceptance Rates

ICFP '11 Paper Acceptance Rate 33 of 92 submissions, 36%;

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
525
Total Downloads

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

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Berger FSchimpf ABieniusa AWehr SFernandez-Reyes KVoinea A(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
https://dl.acm.org/doi/10.1145/3677995.3678189
Castagna GLaurent MNguyễn K(2024)Polymorphic Type Inference for Dynamic LanguagesProceedings of the ACM on Programming Languages10.1145/36328828:POPL(1179-1210)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632882
Castagna G(2023)Typing Records, Maps, and StructsProceedings of the ACM on Programming Languages10.1145/36078387:ICFP(215-258)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607838
Xu HHuang XOliveira B(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
https://dl.acm.org/doi/10.1145/3571224
Castagna G(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
https://doi.org/10.1007/978-3-031-34518-0_12
Schimpf AWehr SBieniusa A(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
https://dl.acm.org/doi/10.1145/3587216.3587220
Castagna GLaurent MNguyễn KLutze M(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
https://dl.acm.org/doi/10.1145/3498674
Castagna GLanvin VLaurent MNguyen K(2022)Revisiting occurrence typingScience of Computer Programming10.1016/j.scico.2022.102781217:COnline publication date: 1-May-2022
https://dl.acm.org/doi/10.1016/j.scico.2022.102781
Jones ERamsay S(2021)Intensional datatype refinement: with application to scalable verification of pattern-match safetyProceedings of the ACM on Programming Languages10.1145/34343365:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434336
HUANG XZHAO JOLIVEIRA B(2021)Taming the Merge OperatorJournal of Functional Programming10.1017/S095679682100018631Online publication date: 2-Nov-2021
https://doi.org/10.1017/S0956796821000186
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 Table of Contents