Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation
Abstract
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 first part we define and study the explicitly-typed version of the calculus in which type instantiation is driven by explicit instantiation annotations. In particular, we define an explicitly-typed lambda-calculus with intersection types and an efficient evaluation model for it. In the second part, presented in a companion paper, we define a local type inference system that allows the programmer to omit explicit instantiation annotations, and a type reconstruction system that allows the programmer to omit explicit type annotations.
The work presented in the two articles provides the theoretical foundations and technical machinery needed to design and implement higher-order polymorphic functional languages for semi-structured data.
Supplementary Material
References
[1]
H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931--940, 1983.
[2]
V. Benzaken, G. Castagna, and A. Frisch. CDuce: an XML-friendly general purpose language. In ICFP '03. ACM Press, 2003.
[3]
V. Bono, B. Venneri, and L. Bettini. A typed lambda calculus with intersection types. Theor. Comput. Sci., 398(1--3):95--113, 2008.
[4]
G. Castagna, K. Nguyen, and Z. Xu. Polymorphic functions with set-theoretic types. Part 2: Local type inference and type reconstruction. Unpublished manuscript, available at http://hal.archives-ouvertes.fr/hal-00880744, November 2013.
[5]
G. Castagna and Z. Xu. Set-theoretic Foundation of Parametric Polymorphism and Subtyping. In ICFP'11, 2011.
[6]
J. Clark and M. Murata. Relax-NG, 2001. www.relaxng.org.
[7]
M. Coppo, M. Dezani, and B. Venneri. Principal type schemes and lambda-calculus semantics. In To H.B. Curry. Essays on Combinatory Logic, Lambda-calculus and Formalism. Academic Press, 1980.
[8]
J. Dunfield and F. Pfenning. Tridirectional typechecking. In POPL'04. ACM Press, 2004.
[9]
J. Robie et al. Xquery 3.0: An XML query language (working draft 2010/12/14), 2010. http://www.w3.org/TR/xquery-30/.
[10]
A. Frisch. OCaml + XDuce. In ICFP'06, 2006.
[11]
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.
[12]
H. Hosoya, A. Frisch, and G. Castagna. Parametric polymorphism for XML. ACM TOPLAS, 32(1):1--56, 2009.
[13]
L. Liquori and S. Ronchi Della Rocca. Intersection-types à la Church. Inf. Comput., 205(9):1371--1386, 2007.
[14]
B.C. Pierce. Types and Programming Languages. MIT Press, 2002.
[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]
J.C. Reynolds. Design of the programming language Forsythe. Technical Report Carnegie Mellon University-CS-96--146, Carnegie Mellon University, 1996.
[17]
J.C. Reynolds. What do types mean?: from intrinsic to extrinsic semantics. In Programming methodology. Springer, 2003.
[18]
S. Ronchi Della Rocca. Intersection typed lambda-calculus. Electr. Notes Theor. Comput. Sci., 70(1):163--181, 2002.
[19]
M. Sulzmann, K. Zhuo, and M. Lu. XHaskell - Adding Regular Expression Types to Haskell. In IFL, LNCS n. 5083. Springer, 2007.
[20]
J. Vouillon. Polymorphic regular tree types and patterns. In POPL'06, pages 103--114, 2006.
[21]
J.B. Wells, A. Dimock, R. Muller, and F.A. Turbak. A calculus with polymorphic and polyvariant flow types. J. Funct. Program., 12(3):183--227, 2002.
[22]
J.B.Wells and C. Haack. Branching types. In ESOP'02, volume 2305 of LNCS, pages 115--132. Springer, 2002.
[23]
Z. Xu. Parametric Polymorphism for XML Processing Languages. PhD thesis, Université Paris Diderot, 2013. Available at http://tel.archives-ouvertes.fr/tel-00858744.
Index Terms
- Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation
Recommendations
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 LanguagesThis 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 ...
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 LanguagesThis 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, ...
Set-theoretic foundation of parametric polymorphism and subtyping
ICFP '11We 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
January 2014
661 pages
January 2014702 pages
Copyright © 2014 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 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].
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 08 January 2014
Published in SIGPLAN Volume 49, Issue 1
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations34Total Citations
- 523Total Downloads
- Downloads (Last 12 months)12
- Downloads (Last 6 weeks)0
Reflects downloads up to 03 Mar 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in