{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T15:10:37Z","timestamp":1743088237735,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030719944"},{"type":"electronic","value":"9783030719951"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper considers parametricity and its resulting free theorems for nested data types. Rather than representing nested types via their Church encodings in a higher-kinded or dependently typed extension of System F, we adopt a functional programming perspective and design a Hindley-Milner-style calculus with primitives for constructing nested types directly as fixpoints. Our calculus can express all nested types appearing in the literature, including truly nested types. At the term level, it supports primitive pattern matching, map functions, and fold combinators for nested types. Our main contribution is the construction of a parametric model for our calculus. This is both delicate and challenging: to ensure the existence of semantic fixpoints interpreting nested types, and thus to establish a suitable Identity Extension Lemma for our calculus, our type system must explicitly track functoriality of types, and cocontinuity conditions on the functors interpreting them must be appropriately threaded throughout the model construction. We prove that our model satisfies an appropriate Abstraction Theorem and verifies all standard consequences of parametricity for primitive nested types.<\/jats:p>","DOI":"10.1007\/978-3-030-71995-1_17","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:03:39Z","timestamp":1616432619000},"page":"324-343","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Parametricity for Primitive Nested Types"],"prefix":"10.1007","author":[{"given":"Patricia","family":"Johann","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5983-6230","authenticated-orcid":false,"given":"Enrico","family":"Ghiorzi","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Jeffries","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Ad\u00e1mek, J., Rosick\u00fd, J.: Locally Presentable and Accessible Categories. Cambridge University Press (1994)","DOI":"10.1017\/CBO9780511600579"},{"key":"17_CR2","unstructured":"Atkey, R.: Relational Parametricity for Higher Kinds. In: Computer Science Logic, pp. 46\u201361. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik (2012)"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Bainbridge, E. S., Freyd, P. J., Scedrov, A., Scott, P. J.: Functorial Polymorphism. Theoretical Computer Science 70, 35\u201364 (1990)","DOI":"10.1016\/0304-3975(90)90151-7"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Bird, R., Meertens, L.: Nested datatypes. In: Mathematics of Program Construction, pp. 52\u201367. Springer (1998)","DOI":"10.1007\/BFb0054285"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Bird, R., Paterson, R.: Generalised folds for nested datatypes. Formal Aspects of Computing 11, 200\u2013222 (1999)","DOI":"10.1007\/s001650050047"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Birkedal, L., M\u00f8gelberg, R. E.: Categorical models for Abadi and Plotkin\u2019s logic for parametricity. Mathematical Structures in Computer Science 15, 709\u2013772 (2005)","DOI":"10.1017\/S0960129505004834"},{"key":"17_CR7","unstructured":"Cardelli, L: Type Systems. In: CRC Handbook of Computer Science and Engineering, pp. 2208\u20132236. CRC Press (1984)"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Dunphy, B., Reddy, U.: Parametric Limits. In: Logic in Computer Science, pp. 242\u2013252. IEEE (2004)","DOI":"10.1109\/LICS.2004.1319618"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Ghani, N., Johann, P., Nordvall Forsberg, F., Orsanigo, F., Revell, T.: Bifibrational Functorial Semantics for Parametric Polymorphism. Electronic Notes in Theoretical Computer Science 319, 165\u2013181. (2015)","DOI":"10.1016\/j.entcs.2015.12.011"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Gill, A., Launchbury, J., Peyton Jones, S. L.: A short cut to deforestation. In: Functional Programming Languages and Computer Architecture, Proceedings, pp. 223\u2013232. Association for Computing Machinery (1993)","DOI":"10.1145\/165180.165214"},{"key":"17_CR11","unstructured":"Girard, J.-Y.: Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. PhD thesis, University of Paris (1972)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Hasegawa, R.: Categorical data types in parametric polymorphism. Mathematical Structures in Computer Science 4, 71\u2013109 (1994)","DOI":"10.1017\/S0960129500000372"},{"key":"17_CR13","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Elsevier (1999)"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Johann, P.: A Generalization of Short-Cut Fusion and Its Correctness Proof. Higher-Order and Symbolic Computation 15, 273\u2013300 (2002)","DOI":"10.1023\/A:1022982420888"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Johann, P., Ghani, N.: Foundations for Structured Programming with GADTs. In: Principles of Programming Languages, pp. 297\u2013308. Association for Computing Machinery (2008)","DOI":"10.1145\/1328897.1328475"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Johann, P., Ghani, N.: Haskell Programming with Nested Types: A Principled Approach Higher-Order and Symbolic Computation 22(2), 155\u2013189 (2010)","DOI":"10.1007\/s10990-009-9047-7"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Johann, P., Polonsky, A.: Higher-kinded data types: Syntax and Semantics. In: Logic in Computer Science, pp. 1\u201313. IEEE (2019)","DOI":"10.1109\/LICS.2019.8785657"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Johann, P., Polonsky, A.: Deep Induction: Induction Rules for (Truly) Nested Types. In: Foundations of Software Science and Computation Structures, pp. 339\u2013358. Springer (2020)","DOI":"10.1007\/978-3-030-45231-5_18"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Matthes, R.: Map Fusion for Nested Datatypes in Intensional Type Theory. Science of Computer Programming 76(3), 204\u2013224 (2011)","DOI":"10.1016\/j.scico.2010.05.008"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Ma, Q., Reynolds, J. C.: Types, abstraction, and parametric polymorphism, part 2. In: Mathematical Foundations of Program Semantics, pp. 1\u201340. Springer-Verlag (1992)","DOI":"10.1007\/3-540-55511-0_1"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Martin, C., Gibbons, J.: On the semantics of nested datatypes. Information Processing Letters 80(5), 233\u2013238 (2001)","DOI":"10.1016\/S0020-0190(01)00168-5"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Pitts, A.: Parametric polymorphism, recursive types, and operational equivalence. (1998)","DOI":"10.1016\/S1571-0661(05)80685-1"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Pitts, A.: Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10, 321\u2013359 (2000)","DOI":"10.1017\/S0960129500003066"},{"key":"17_CR24","unstructured":"Reynolds, J. C.: Types, abstraction, and parametric polymorphism. Information Processing 83(1), 513\u2013523 (1983)"},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Reynolds, J. C.: Polymorphism is not set-theoretic. Semantics of Data Types, 145\u2013156 (1984)","DOI":"10.1007\/3-540-13346-1_7"},{"key":"17_CR26","unstructured":"Robinson, E., Rosolini, G.: Reflexive graphs and parametric polymorphism. In: Logic in Computer Science, pp. 364\u2013371. IEEE (1994)"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Theorems for free!. In: Functional Programming Languages and Computer Architecture, Proceedings, pp. 347\u2013359. Association for Computing Machinery (1989)","DOI":"10.1145\/99370.99404"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-71995-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:07:21Z","timestamp":1616432841000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-71995-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030719944","9783030719951"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-71995-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FOSSACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"88","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}