Document Open Access Logo

Strongly Normalizing Higher-Order Relational Queries

Authors Wilmer Ricciotti , James Cheney

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.28.pdf
  • Filesize: 0.58 MB
  • 22 pages

Document Identifiers

Author Details

Wilmer Ricciotti
  • Laboratory for Foundations of Computer Science, University of Edinburgh, UK
James Cheney
  • Laboratory for Foundations of Computer Science, University of Edinburgh, UK

Funding

This work was supported by ERC Consolidator Grant Skye (grant number ERC-682315), a grant from the UK Research Institute in Verified Trustworthy Software Systems (VeTSS), and by an ISCF Metrology Fellowship grant provided by the UK government’s Department for Business, Energy and Industrial Strategy (BEIS).

Acknowledgements

We are grateful to Philip Wadler, Sam Lindley, and the anonymous reviewers for their comments and suggestions.

Cite As Get BibTex

Wilmer Ricciotti and James Cheney. Strongly Normalizing Higher-Order Relational Queries. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 28:1-28:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.FSCD.2020.28

Abstract

Language-integrated query is a powerful programming construct allowing database queries and ordinary program code to interoperate seamlessly and safely. Language-integrated query techniques rely on classical results about monadic comprehension calculi, including the conservativity theorem for nested relational calculus. Conservativity implies that query expressions can freely use nesting and unnesting, yet as long as the query result type is a flat relation, these capabilities do not lead to an increase in expressiveness over flat relational queries. Wong showed how such queries can be translated to SQL via a constructive rewriting algorithm, and Cooper and others advocated higher-order nested relational calculi as a basis for language-integrated queries in functional languages such as Links and F#. However there is no published proof of the central strong normalization property for higher-order nested relational queries: a previous proof attempt does not deal correctly with rewrite rules that duplicate subterms. This paper fills the gap in the literature, explaining the difficulty with a previous proof attempt, and showing how to extend the ⊤⊤-lifting approach of Lindley and Stark to accommodate duplicating rewrites. We also sketch how to extend the proof to a recently-introduced calculus for heterogeneous queries mixing set and multiset semantics.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Strong normalization
  • ⊤⊤-lifting
  • Nested relational calculus
  • Language-integrated query

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Véronique Benzaken and Evelyne Contejean. A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra. In CPP 2019, pages 249-261, 2019. URL: http://dx.doi.org/10.1145/3293880.3294107.
  2. Peter Buneman, Shamim Naqvi, Val Tannen, and Limsoon Wong. Principles of programming with complex objects and collection types. Theor. Comput. Sci., 149(1), 1995. URL: http://dx.doi.org/10.1016/0304-3975(95)00024-Q.
  3. James Cheney, Sam Lindley, and Philip Wadler. A practical theory of language-integrated query. In ICFP, 2013. URL: http://dx.doi.org/10.1145/2500365.2500586.
  4. James Cheney, Sam Lindley, and Philip Wadler. Query shredding: efficient relational evaluation of queries over nested multisets. In SIGMOD, pages 1027-1038. ACM, 2014. URL: http://dx.doi.org/10.1145/2588555.2612186.
  5. Shumo Chu, Konstantin Weitz, Alvin Cheung, and Dan Suciu. HoTTSQL: Proving query rewrites with univalent SQL semantics. In PLDI, pages 510-524. ACM, 2017. URL: http://dx.doi.org/10.1145/3062341.3062348.
  6. Ezra Cooper. Programming language features for web application development. PhD thesis, University of Edinburgh, 2009. Google Scholar
  7. Ezra Cooper. The script-writer’s dream: How to write great SQL in your own language, and be sure it will succeed. In DBPL, 2009. URL: http://dx.doi.org/10.1007/978-3-642-03793-1_3.
  8. Ezra Cooper, Sam Lindley, Philip Wadler, and Jeremy Yallop. Links: web programming without tiers. In FMCO, 2007. URL: http://dx.doi.org/10.1007/978-3-540-74792-5_12.
  9. Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1989. Google Scholar
  10. Paolo Guagliardo and Leonid Libkin. A formal semantics of SQL queries, its validation, and applications. PVLDB, 2017. URL: http://dx.doi.org/10.14778/3151113.3151116.
  11. Oleg Kiselyov and Tatsuya Katsushima. Sound and efficient language-integrated query - maintaining the ORDER. In APLAS 2017, pages 364-383, 2017. URL: http://dx.doi.org/10.1007/978-3-319-71237-6_18.
  12. Leonid Libkin and Limsoon Wong. Conservativity of nested relational calculi with internal generic functions. Inf. Process. Lett., 49(6):273-280, 1994. URL: http://dx.doi.org/10.1016/0020-0190(94)90099-X.
  13. Leonid Libkin and Limsoon Wong. Query languages for bags and aggregate functions. J. Comput. Syst. Sci., 55(2), 1997. URL: http://dx.doi.org/10.1006/jcss.1997.1523.
  14. Sam Lindley and James Cheney. Row-based effect types for database integration. In TLDI, 2012. URL: http://dx.doi.org/10.1145/2103786.2103798.
  15. Sam Lindley and Ian Stark. Reducibility and ⊤⊤-lifting for computation types. In TLCA, 2005. URL: http://dx.doi.org/10.1007/11417170_20.
  16. Erik Meijer, Brian Beckman, and Gavin M. Bierman. LINQ: reconciling object, relations and XML in the .NET framework. In SIGMOD, 2006. URL: http://dx.doi.org/10.1145/1142473.1142552.
  17. Jan Paredaens and Dirk Van Gucht. Converting nested algebra expressions into flat algebra expressions. ACM Trans. Database Syst., 17(1), 1992. URL: http://dx.doi.org/10.1145/128765.128768.
  18. Andrew M. Pitts. Parametric polymorphism and operational equivalence (preliminary version). In HOOTS II, volume 10, pages 2-27, 1998. URL: http://dx.doi.org/10.1016/S1571-0661(05)80685-1.
  19. W. Ricciotti and J. Cheney. Strongly Normalizing Audited Computation. In V. Goranko and M. Dam, editors, CSL 2017, volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 36:1-36:21. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2017.36.
  20. Wilmer Ricciotti and James Cheney. Mixing set and bag semantics. In DBPL, pages 70-73, 2019. URL: http://dx.doi.org/10.1145/3315507.3330202.
  21. Philip Trinder and Philip Wadler. Improving list comprehension database queries. In TENCON '89., 1989. URL: http://dx.doi.org/10.1109/TENCON.1989.176921.
  22. Philip Wadler. Comprehending monads. Math. Struct. in Comp. Sci., 2(4), 1992. URL: http://dx.doi.org/10.1017/S0960129500001560.
  23. Limsoon Wong. Normal forms and conservative extension properties for query languages over collection types. J. Comput. Syst. Sci., 52(3), 1996. URL: http://dx.doi.org/10.1006/jcss.1996.0037.
  24. Limsoon Wong. Kleisli, a functional query system. J. Funct. Programming, 10(1), 2000. URL: http://dx.doi.org/10.1017/S0956796899003585.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact