{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:42Z","timestamp":1747173462758,"version":"3.40.5"},"reference-count":52,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T00:00:00Z","timestamp":1634774400000},"content-version":"unspecified","delay-in-days":293,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In verified generic programming, one cannot exploit the structure of concrete data types but has to rely on<jats:italic>well chosen<\/jats:italic>sets of specifications or abstract data types (ADTs). Functors and monads are at the core of many applications of functional programming. This raises the question of what useful ADTs for verified functors and monads could look like. The functorial map of many important monads preserves extensional equality. For instance, if<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0956796821000204_inline1.png\"\/><jats:tex-math>$$f,g \\, : \\, A \\, \\to \\, B$$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>are extensionally equal, that is,<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0956796821000204_inline2.png\"\/><jats:tex-math>$$\\forall x \\in A$$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>,<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0956796821000204_inline3.png\"\/><jats:tex-math>$$f \\, x = g \\, x$$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, then<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0956796821000204_inline4.png\"\/><jats:tex-math>$$map \\, f \\, : \\, List \\, A \\to List \\, B$$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>and<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0956796821000204_inline5.png\"\/><jats:tex-math>$$map \\, g$$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>are also extensionally equal. This suggests that<jats:italic>preservation of extensional equality<\/jats:italic>could be a useful principle in verified generic programming. We explore this possibility with a minimalist approach: we deal with (the lack of) extensional equality in Martin-L\u00f6f\u2019s intensional type theories without extending the theories or using full-fledged setoids. Perhaps surprisingly, this minimal approach turns out to be extremely useful. It allows one to derive simple generic proofs of monadic laws but also verified, generic results in dynamical systems and control theory. In turn, these results avoid tedious code duplication and ad-hoc proofs. Thus, our work is a contribution toward pragmatic, verified generic programming.<\/jats:p>","DOI":"10.1017\/s0956796821000204","type":"journal-article","created":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T12:41:46Z","timestamp":1634820106000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":2,"title":["Extensional equality preservation and verified generic programming"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8923-2734","authenticated-orcid":false,"given":"NICOLA","family":"BOTTA","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4435-7960","authenticated-orcid":false,"given":"NURIA","family":"BREDE","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3078-1437","authenticated-orcid":false,"given":"PATRIK","family":"JANSSON","sequence":"additional","affiliation":[]},{"given":"TIM","family":"RICHTER","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2021,10,21]]},"reference":[{"doi-asserted-by":"publisher","key":"S0956796821000204_ref21","DOI":"10.1109\/LICS.1994.316071"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref26","DOI":"10.1016\/S0167-6423(01)00020-X"},{"unstructured":"Blanqui, F. , et al. (2020) CoLoR: A Coq Library on Rewriting and termination (Version 1.8.0). Available at: https:\/\/github.com\/fblanqui\/color","key":"S0956796821000204_ref7"},{"volume-title":"Prentice Hall International Series in Computer Science","year":"1997","author":"Bird","key":"S0956796821000204_ref5"},{"unstructured":"Hofmann, M. (1995 ) Extensional Concepts in Intensional Type Theory. PhD thesis, University of Edinburgh.","key":"S0956796821000204_ref20"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref13","DOI":"10.1007\/978-3-319-08434-3_19"},{"unstructured":"JetBrains Research. (2021) Arend Theorem Prover (Version 1.6.0). Available at: https:\/\/arend-lang.github.io\/","key":"S0956796821000204_ref27"},{"unstructured":"Ionescu, C. (2009) Vulnerability Modelling and Monadic Dynamical Systems. PhD thesis, Freie Universit\u00e4t Berlin.","key":"S0956796821000204_ref24"},{"unstructured":"Martin-L\u00f6f, P. & Sambin, G. (1984) Intuitionistic Type Theory, vol. 9. Bibliopolis Naples.","key":"S0956796821000204_ref31"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref22","DOI":"10.1145\/3437992.3439922"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref34","DOI":"10.1017\/S0956796809007345"},{"unstructured":"Streicher, T. (1993) Investigations into Intensional Type Theory. Habilitiation Thesis, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen.","key":"S0956796821000204_ref42"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref2","DOI":"10.1007\/978-3-030-14805-8_4"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref9","DOI":"10.1145\/3018610.3018620"},{"key":"S0956796821000204_ref39","first-page":"41","article-title":"A new look at generalized rewriting in type theory","volume":"2","author":"Sozeau","year":"2010","journal-title":"J. Formal. Reason."},{"key":"S0956796821000204_ref30","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-9860-1","volume-title":"Algebraic Theories","author":"Manes","year":"1976"},{"volume-title":"Type-Driven Development in Idris","year":"2017","author":"Brady","key":"S0956796821000204_ref10"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref16","DOI":"10.1007\/BFb0026809"},{"unstructured":"Megacz, A. (2011) Category Theory in Coq (Coq-Categories). Available at: http:\/\/www.megacz.com\/berkeley\/coq-categories\/","key":"S0956796821000204_ref33"},{"doi-asserted-by":"crossref","unstructured":"Giry, M. (1981) A categorial approach to probability theory. In Categorical Aspects of Topology and Analysis, Banaschewski, B. (ed). Lecture Notes in Mathematics 915. Springer, pp. 68\u201385.","key":"S0956796821000204_ref18","DOI":"10.1007\/BFb0092872"},{"unstructured":"Streicher, T. (2003) Category Theory and Categorical Logic. Lecture Notes, Technische Universit\u00e4t Darmstadt. Available at: https:\/\/www2.mathematik.tu-darmstadt.de\/ streicher\/CTCL.pdf.","key":"S0956796821000204_ref43"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref17","DOI":"10.1017\/S0956796805005721"},{"doi-asserted-by":"crossref","unstructured":"Brede, N. & Botta, N. (2021) On the Correctness of Monadic Backward Induction. Submitted to Journal of Functional Programming, Available at: https:\/\/arxiv.org\/abs\/2008.02143","key":"S0956796821000204_ref11","DOI":"10.1017\/S0956796821000228"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref8","DOI":"10.1017\/S0956796817000156"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref44","DOI":"10.5281\/zenodo.4501022"},{"unstructured":"Carette, J. & Hu, J. Z. S. (2021) A new Categories library for Agda (Version 0.1.5). https:\/\/github.com\/agda\/agda-categories","key":"S0956796821000204_ref12"},{"unstructured":"The Idris Community. (2020) Documentation for the Idris Language. Available at: http:\/\/docs.idris-lang.org\/en\/latest\/","key":"S0956796821000204_ref45"},{"volume-title":"Catastrophe Theory","year":"2012","author":"Thomas","key":"S0956796821000204_ref47"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref51","DOI":"10.1145\/143165.143169"},{"unstructured":"Ionescu, C. & Jansson, P. (2013) Testing versus proving in climate impact research. In Proc. TYPES 2011. Leibniz International Proceedings in Informatics (LIPIcs) 19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, pp. 41\u201354.","key":"S0956796821000204_ref25"},{"volume-title":"Foundations of Constructive Analysis","year":"1967","author":"Bishop","key":"S0956796821000204_ref6"},{"volume-title":"Elements of Applied Bifurcation Theory","year":"1998","author":"Kuznetsov","key":"S0956796821000204_ref29"},{"unstructured":"Peyton Jones, S. , Tolmach, A. & Hoare, T. (2001) Playing by the rules: Rewriting as a practical optimisation technique in GHC. In 2001 Haskell Workshop, pp. 203\u2013233. ACM SIGPLAN.","key":"S0956796821000204_ref37"},{"volume-title":"Foundations of Computing Series","year":"1991","author":"Pierce","key":"S0956796821000204_ref38"},{"unstructured":"The Univalent Foundations Program. (2013) Homotopy Type Theory: Univalent Foundations of Mathematics. Available at: https:\/\/homotopytypetheory.org\/book","key":"S0956796821000204_ref46"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref48","DOI":"10.1017\/S0956796821000034"},{"unstructured":"Voevodsky, V. , Ahrens, B. , Grayson, D. , et al.. (2021) UniMath \u2014 A Computer-Checked Library of Univalent mathematics. Available at https:\/\/github.com\/UniMath\/UniMath","key":"S0956796821000204_ref49"},{"doi-asserted-by":"crossref","unstructured":"Huet, G. & Sa\u00efbi, A. (2000) Constructive category theory. In Proof, Language, and Interaction. Essays in Honor of Robin Milnor, Plotkin, G., Stirling, C. & Tofte, M. (eds). MIT, pp. 239\u2013275.","key":"S0956796821000204_ref23","DOI":"10.7551\/mitpress\/5641.003.0015"},{"unstructured":"von Glehn, T. (2015) Polynomials and Models of Type Theory. PhD thesis, University of Cambridge.","key":"S0956796821000204_ref50"},{"unstructured":"Wiegley, J. (2018) Category Theory in Coq. Available from https:\/\/github.com\/jwiegley\/category-theory","key":"S0956796821000204_ref52"},{"unstructured":"Spitters, B. & Semeria, V. M. (2017) Coq Repository at Nijmegen (Version 1.2.0). Available at: https:\/\/github.com\/coq-community\/corn","key":"S0956796821000204_ref40"},{"key":"S0956796821000204_ref35","volume-title":"International Series of Monographs on Computer Science","volume":"200","author":"Nordstr\u00f6m","year":"1990"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref19","DOI":"10.1145\/322276.322285"},{"key":"S0956796821000204_ref15","first-page":"206","volume-title":"ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2006)","author":"Danielsson","year":"2006"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref28","DOI":"10.1145\/2364506.2364514"},{"key":"S0956796821000204_ref32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0956796807006326","article-title":"Applicative programming with effects","volume":"18","author":"McBride","year":"2008","journal-title":"J. Funct. Program."},{"volume-title":"Dynamic Programming","year":"1957","author":"Bellman","key":"S0956796821000204_ref3"},{"unstructured":"Altenkirch, T. (2017) From setoid hell to homotopy heaven? Available at: https:\/\/www.cs.nott.ac.uk\/ psztxa\/talks\/types-17-hell.pdf","key":"S0956796821000204_ref1"},{"unstructured":"Norell, U. (2007) Towards a Practical Programming Language Based on Dependent Type theory. PhD thesis, Chalmers University of Technology.","key":"S0956796821000204_ref36"},{"volume-title":"Theoretical Computer Science","year":"1991","author":"Streicher","key":"S0956796821000204_ref41"},{"doi-asserted-by":"publisher","key":"S0956796821000204_ref4","DOI":"10.1017\/CBO9781316092415"},{"unstructured":"Cohen, C. , Coquand, T. , Huber, S. & M\u00f6rtberg, A. (2018) Cubical type theory: A constructive interpretation of the univalence axiom. In Proc. TYPES 2015. Leibniz International Proceedings in Informatics (LIPIcs) 69, pp. 5:1\u20135:34. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik.","key":"S0956796821000204_ref14"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796821000204","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T11:46:59Z","timestamp":1725968819000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796821000204\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"references-count":52,"alternative-id":["S0956796821000204"],"URL":"https:\/\/doi.org\/10.1017\/s0956796821000204","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"type":"print","value":"0956-7968"},{"type":"electronic","value":"1469-7653"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e24"}}