research-article

Open access

A Logical Approach to Deciding Semantic Subtyping

Authors:

Nils Gesbert,

Pierre Genevès,

Nabil LayaïdaAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 38, Issue 1

Article No.: 3, Pages 1 - 31

https://doi.org/10.1145/2812805

Published: 16 October 2015 Publication History

PDF eReader

Abstract

We consider a type algebra equipped with recursive, product, function, intersection, union, and complement types, together with type variables. We consider the subtyping relation defined by Castagna and Xu [2011] over such type expressions and show how this relation can be decided in EXPTIME, answering an open question. The novelty, originality and strength of our solution reside in introducing a logical modeling for the semantic subtyping framework. We model semantic subtyping in a tree logic and use a satisfiability-testing algorithm in order to decide subtyping. We report on practical experiments made with a full implementation of the system. This provides a powerful polymorphic type system aiming at maintaining full static type-safety of functional programs that manipulate trees, even with higher-order functions, which is particularly useful in the context of XML.

References

[1]

Michael Benedikt and James Cheney. 2010. Destabilizers and independence of XML updates. Proceedings of the VLDB Endowment 3, 1, 906--917.

Digital Library

Google Scholar

[2]

Véronique Benzaken, Giuseppe Castagna, and Alain Frisch. 2003. CDuce: An XML-centric general-purpose language. In Proceedings of the 8th International Conference on Functional Programming (ICFP’03). Uppsala, Sweden, 51--63. http://doi.acm.org/10.1145/944705.944711

Digital Library

Google Scholar

[3]

Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, and David Langworthy. 2010. Semantic subtyping with an SMT solver. In Proceedings of the 15th International Conference on Functional Programming (ICFP’10). Baltimore, MD, 105--116. http://doi.acm.org/10.1145/1863543.1863560

Digital Library

Google Scholar

[4]

Scott Boag, Don Chamberlin, Mary F. Fernández, Daniela Florescu, Jonathan Robie, and Jérôme Siméon. 2007. XQuery 1.0: An XML Query Language, W3C Recommendation.

Google Scholar

[5]

Randal E. Bryant. 1986. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers 35, 8, 677--691.

Digital Library

Google Scholar

[6]

Cristiano Calcagno, Luca Cardelli, and Andrew D. Gordon. 2005. Deciding validity in a spatial logic for trees. Journal of Functional Programming 15, 4, 543--572.

Digital Library

Google Scholar

[7]

Luca Cardelli and Andrew D. Gordon. 2000. Anytime, anywhere: Modal logics for mobile ambients. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’00). ACM, New York, NY, 365--377.

Digital Library

Google Scholar

[8]

Giuseppe Castagna and Zhiwu Xu. 2011. Set-theoretic foundation of parametric polymorphism and subtyping. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP’11). ACM, Tokyo, 94--106.

Digital Library

Google Scholar

[9]

James Clark and Steve DeRose. 1999. XML Path Language (XPath) Version 1.0, W3C Recommendation. Retrieved August 31, 2015 from http://www.w3.org/TR/1999/REC-xpath-19991116.

Google Scholar

[10]

Edmund M. Clarke Jr., Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, MA.

Digital Library

Google Scholar

[11]

Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08). Budapest, 337--340. http://dx.doi.org/10.1007/978-3-540-78800-3_24.

Crossref

Google Scholar

[12]

A. Frisch, G. Castagna, and V. Benzaken. 2008. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM 55, 4, 1--64.

Digital Library

Google Scholar

[13]

Pierre Genevès. 2006. Logics for XML. Ph.D. Dissertation. Institut National Polytechnique de Grenoble. Retrieved August 31, 2015 from http://wam.inrialpes.fr/publications/2006/geneves-phd.pdf.

Google Scholar

[14]

Pierre Genevès, Nabil Layaïda, and Vincent Quint. 2009. Identifying query incompatibilities with evolving XML schemas. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP’09). ACM, New York, NY, 221--230.

Digital Library

Google Scholar

[15]

Pierre Genevès, Nabil Layaïda, and Alan Schmitt. 2007. Efficient static analysis of XML paths and types. In Proceedings of the 28th Conference on Programming Language Design and iImplementation (PLDI’07). San Diego, CA, 342--351. http://doi.acm.org/10.1145/1250734.1250773

Digital Library

Google Scholar

[16]

Pierre Genevès, Nabil Layaïda, Alan Schmitt, and Nils Gesbert. 2015. Efficiently deciding μ-calculus with converse over finite trees. ACM Transactions on Computational Logic 16, 2, 16:1--16:41.

Digital Library

Google Scholar

[17]

Nils Gesbert, Pierre Genevès, and Nabil Layaïda. 2011. Parametric polymorphism and semantic subtyping: The logical connection. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP’11). ACM, Tokyo, 107--116.

Digital Library

Google Scholar

[18]

H. Hosoya, A. Frisch, and G. Castagna. 2009. Parametric polymorphism for XML. ACM Transactions on Programming Languages and Systems 32, 1, 1--56.

Digital Library

Google Scholar

[19]

Haruo Hosoya and Benjamin C. Pierce. 2003. XDuce: A statically typed XML processing language. ACM Transactions on Internet Technology 3, 2, 117--148. http://doi.acm.org/10.1145/767193.767195

Digital Library

Google Scholar

[20]

Haruo Hosoya, Jérôme Vouillon, and Benjamin C. Pierce. 2005. Regular expression types for XML. ACM Transactions on Programming Languages and Systems 27, 1, 46--90. http://doi.acm.org/10.1145/1053468.1053470.

Digital Library

Google Scholar

[21]

Gérard P. Huet. 1997. The zipper. Journal of Functional Programming 7, 5, 549--554.

Digital Library

Google Scholar

[22]

Barbara Liskov and Jeannette M. Wing. 1994. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems 16, 6, 1811--1841.

Digital Library

Google Scholar

[23]

R. Milner, L. Morris, and M. Newey. 1975. A logic for computable functions with reflexive and polymorphic types. In Conference on Proving and Improving Programs, Arc-et-Senans, France. IRIA-Laboria, 78150 Le Chesnay, France, 371--394.

Google Scholar

[24]

Guoqiang Pan, Ulrike Sattler, and Moshe Y. Vardi. 2006. BDD-based decision procedures for the modal logic K. Journal of Applied Non-classical Logics 16, 1--2, 169--208.

Crossref

Google Scholar

[25]

John C. Reynolds. 1983. Types, abstraction and parametric polymorphism. In IFIP Congress. 513--523.

Google Scholar

[26]

Jonathan Robie, Don Chamberlin, Michael Dyck, and John Snelson. 2014. XQuery 3.0: An XML Query Language, W3C Recommendation. Retrieved August 31, 2015 from http://www.w3.org/TR/xquery-30/.

Google Scholar

[27]

Jérôme Vouillon. 2006. Polymorphic regular tree types and patterns. In Proceedings of the 33rd Symposium on Principles of Programming Languages (POPL’06). 103--114. http://doi.acm.org/10.1145/1111037.1111047.

Digital Library

Google Scholar

Cited By

View all

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)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
Castagna GLanvin VPetrucciani TSiek J(2019)Gradual typing: a new perspectiveProceedings of the ACM on Programming Languages10.1145/32903293:POPL(1-32)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290329
Show More Cited By

Index Terms

A Logical Approach to Deciding Semantic Subtyping
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Polymorphism
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

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 ...
On the power of coercion abstraction
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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 ...
System F with coercion constraints
CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

We present a second-order λ-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions ...

Reviews

Reviewer: Richard John Botting

Although object-oriented subtyping has been efficiently resolved by compilers for years, this paper shows how subtyping in Extensible Markup Language (XML)-centric functional languages can be done with a SAT solver. It gives a tested formal specification for an efficient algorithm if such exists. The paper is the result of a decade of research, which is documented in the references. It will mainly interest graduate students and professors working in type theory and logic. A SAT solver is a subprogram that either finds values for variables in a logical formula that satisfy it (make it true) or reports that they don't exist. The worst-case time for all known SAT solvers grows exponentially with the size of the formula. The author's paradigm is: 1) clearly define the property; 2) encode the property as a logical formula; 3) tune the formula; and 4) use a SAT solver on the formula. These steps are applied to testing if one LISP-like data type is a subtype of another one. The paper uses semantic subtyping. This is where one type is defined to be a subtype of another if all data of one type are elements of the other type. The types include function types, types defined by parametric (not object-oriented) polymorphism, and types defined by recursion. The authors' logical model handles all of these. The resulting software has been tested and works well. They show that it has the same complexity as the SAT solver used. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 38, Issue 1

October 2015

88 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/2836326

Editor:
Jens Palsberg
University of California, Los Angeles, USA

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: 16 October 2015

Accepted: 01 August 2015

Received: 01 April 2015

Published in TOPLAS Volume 38, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Agence Nationale de la Recherche

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
313
Total Downloads

Downloads (Last 12 months)39
Downloads (Last 6 weeks)7

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

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)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
Castagna GLanvin VPetrucciani TSiek J(2019)Gradual typing: a new perspectiveProceedings of the ACM on Programming Languages10.1145/32903293:POPL(1-32)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290329
Muehlboeck FTate R(2018)Empowering union and intersection types with integrated subtypingProceedings of the ACM on Programming Languages10.1145/32764822:OOPSLA(1-29)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276482

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations

On the power of coercion abstraction

On the power of coercion abstraction

System F with coercion constraints

Reviews

Access critical reviews of Computing literature here

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Funding Sources

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations