Article

Polymorphic regular tree types and patterns

Author:

Jérôme VouillonAuthors Info & Claims

POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 103 - 114

https://doi.org/10.1145/1111037.1111047

Published: 11 January 2006 Publication History

Get Access

Abstract

We propose a type system based on regular tree grammars, where algebraic datatypes are interpreted in a structural way. Thus, the same constructors can be reused for different types and a flexible subtyping relation can be defined between types, corresponding to the inclusion of their semantics. For instance, one can define a type for lists and a subtype of this type corresponding to lists of even length. Patterns are simply types annotated with binders. This provides a generalization of algebraic patterns with the ability of matching arbitrarily deep in a value. Our main contribution, compared to languages such as XDuce and CDuce, is that we are able to deal with both polymorphism and function types.

References

[1]

M. Brandt and F. Henglein. Coinductive axiomatization of recursive type equality and subtyping. In R. Hindley, editor, Proc. 3d Int'l Conf. on Typed Lambda Calculi and Applications (TLCA), Nancy, France, April 2-4, 1997, volume 1210 of Lecture Notes in Computer Science (LNCS), pages 63--81. Springer-Verlag, April 1997.

Digital Library

Google Scholar

[2]

R. Cartwright. Types as intervals. In Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 22--36. ACM Press, 1985.

Digital Library

Google Scholar

[3]

CDuce Development Team. CDuce Programming Language User's Manual. Available from http://www.cduce.org/documentation.html.

Google Scholar

[4]

A. Frisch. Théorie, conception et réalisation d'un langage adapté à XML. Thèse de doctorat, University of Paris 7, 2004.

Google Scholar

[5]

V. Gapeyev, M. Levin, and B. Pierce. Recursive subtyping revealed. Journal of Functional Programming, 12(6):511--548, 2003. Preliminary version in ICFP 2000.

Digital Library

Google Scholar

[6]

H. Hosoya, A. Frisch, and G. Castagna. Parametric polymorphism for XML. In POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT sysposium on Principles of programming languages, pages 50--62. ACM Press, 2005.

Digital Library

Google Scholar

[7]

H. Hosoya and B. C. Pierce. XDuce: A statically typed XML processing language. ACM Transactions on Internet Technology, 3(2):117--148, May 2003.

Digital Library

Google Scholar

[8]

H. Hosoya, J. Vouillon, and B. C. Pierce. Regular expression types for XML. ACM Trans. Program. Lang. Syst., 27(1):46--90, 2005. Short version in ICFP 2000.

Digital Library

Google Scholar

[9]

M. Y. Levin. Compiling regular patterns. In ICFP '03: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, pages 65--77, New York, NY, USA, 2003. ACM Press.

Digital Library

Google Scholar

[10]

J. C. Reynolds. Types, abstraction, and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513--523, Amsterdam, 1983. Elsevier Science Publishers B. V. (North-Holland).

Google Scholar

[11]

A. K. Wright. Simple imperative polymorphism. Lisp Symb. Comput., 8(4):343--355, 1995.

Digital Library

Google Scholar

Cited By

View all

Chen HZhiwu X(2020)Inclusion algorithms for one-unambiguous regular expressions and their applicationsScience of Computer Programming10.1016/j.scico.2020.102436(102436)Online publication date: Mar-2020
https://doi.org/10.1016/j.scico.2020.102436
Shvedenko VShvedenko VShchekochikhin O(2019)Using Structural and Parametric Polymorphism in the Creation of Digital TwinsAutomatic Documentation and Mathematical Linguistics10.3103/S000510551902005553:2(81-84)Online publication date: 1-Mar-2019
https://dl.acm.org/doi/10.3103/S0005105519020055
Benzaken VCastagna GHosoya HPierce BVansummeren S(2018)XML TypecheckingEncyclopedia of Database Systems10.1007/978-1-4614-8265-9_788(4817-4822)Online publication date: 7-Dec-2018
https://doi.org/10.1007/978-1-4614-8265-9_788
Show More Cited By

Index Terms

Polymorphic regular tree types and patterns
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
        Patterns
        Polymorphism
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Polymorphic regular tree types and patterns
Proceedings of the 2006 POPL Conference

We propose a type system based on regular tree grammars, where algebraic datatypes are interpreted in a structural way. Thus, the same constructors can be reused for different types and a flexible subtyping relation can be defined between types, ...
Optimal Representations of Polymorphic Types with Subtyping

Many type inference and program analysis systems include notions of subtyping and parametric polymorphism. When used together, these two features induce equivalences that allow types to be simplified by eliminating quantified variables. Eliminating ...
On the power of coercion abstraction
POPL '12

Erasable coercions in System F-eta, also known as retyping functions, are well-typed eta-expansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in F-eta can model ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2006

432 pages

ISBN:1595930272

DOI:10.1145/1111037

General Chair:
Greg Morrisett
Harvard University, USA
,
Program Chair:
Simon Peyton Jones
Microsoft Research, UK

ACM SIGPLAN Notices Volume 41, Issue 1
Proceedings of the 2006 POPL Conference
January 2006
421 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1111320
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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL06

Sponsor:

POPL06: The 33rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2006

January 11 - 13, 2006

South Carolina, Charleston, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
472
Total Downloads

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

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Chen HZhiwu X(2020)Inclusion algorithms for one-unambiguous regular expressions and their applicationsScience of Computer Programming10.1016/j.scico.2020.102436(102436)Online publication date: Mar-2020
https://doi.org/10.1016/j.scico.2020.102436
Shvedenko VShvedenko VShchekochikhin O(2019)Using Structural and Parametric Polymorphism in the Creation of Digital TwinsAutomatic Documentation and Mathematical Linguistics10.3103/S000510551902005553:2(81-84)Online publication date: 1-Mar-2019
https://dl.acm.org/doi/10.3103/S0005105519020055
Benzaken VCastagna GHosoya HPierce BVansummeren S(2018)XML TypecheckingEncyclopedia of Database Systems10.1007/978-1-4614-8265-9_788(4817-4822)Online publication date: 7-Dec-2018
https://doi.org/10.1007/978-1-4614-8265-9_788
Ligatti JBlackburn JNachtigal M(2017)On Subtyping-Relation Completeness, with an Application to Iso-Recursive TypesACM Transactions on Programming Languages and Systems10.1145/299459639:1(1-36)Online publication date: 6-Mar-2017
https://dl.acm.org/doi/10.1145/2994596
Benzaken VCastagna GHosoya HPierce BVansummeren S(2016)XML TypecheckingEncyclopedia of Database Systems10.1007/978-1-4899-7993-3_788-2(1-6)Online publication date: 29-Dec-2016
https://doi.org/10.1007/978-1-4899-7993-3_788-2
Gesbert NGenevès PLayaïda N(2015)A Logical Approach to Deciding Semantic SubtypingACM Transactions on Programming Languages and Systems10.1145/281280538:1(1-31)Online publication date: 16-Oct-2015
https://dl.acm.org/doi/10.1145/2812805
Castagna GNguyen KXu ZIm HLenglet SPadovani L(2014)Polymorphic functions with set-theoretic typesACM SIGPLAN Notices10.1145/2578855.253584049:1(5-17)Online publication date: 8-Jan-2014
https://dl.acm.org/doi/10.1145/2578855.2535840
Castagna GNguyen KXu ZIm HLenglet SPadovani LJagannathan SSewell P(2014)Polymorphic functions with set-theoretic typesProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2535838.2535840(5-17)Online publication date: 11-Jan-2014
https://dl.acm.org/doi/10.1145/2535838.2535840
Gesbert NGenevès PLayaïda NChakravarty MHu ZDanvy O(2011)Parametric polymorphism and semantic subtypingProceedings of the 16th ACM SIGPLAN international conference on Functional programming10.1145/2034773.2034789(107-116)Online publication date: 19-Sep-2011
https://dl.acm.org/doi/10.1145/2034773.2034789
Castagna GXu ZChakravarty MHu ZDanvy O(2011)Set-theoretic foundation of parametric polymorphism and subtypingProceedings of the 16th ACM SIGPLAN international conference on Functional programming10.1145/2034773.2034788(94-106)Online publication date: 19-Sep-2011
https://dl.acm.org/doi/10.1145/2034773.2034788
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.

Cited By

Index Terms

Recommendations

Polymorphic regular tree types and patterns

Optimal Representations of Polymorphic Types with Subtyping

On the power of coercion abstraction