{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T21:17:43Z","timestamp":1764364663375,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031300431"},{"type":"electronic","value":"9783031300448"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,17]],"date-time":"2023-04-17T00:00:00Z","timestamp":1681689600000},"content-version":"vor","delay-in-days":106,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>State of the art optimisation passes for dependently typed languages can help erase the redundant information typical of invariant-rich data structures and programs. These automated processes do not dramatically change the <jats:italic>structure<\/jats:italic> of the data, even though more efficient representations could be available.<\/jats:p><jats:p>Using Quantitative Type Theory as implemented in Idris 2, we demonstrate how to define an invariant-rich, typechecking-time data structure packing an efficient runtime representation together with runtime irrelevant invariants. The compiler can then aggressively erase all such invariants during compilation.<\/jats:p><jats:p>Unlike other approaches, the complexity of the resulting representation is entirely predictable, we do not require both representations to have the same structure, and yet we are able to seamlessly program as if we were using the high-level structure.<\/jats:p>","DOI":"10.1007\/978-3-031-30044-8_5","type":"book-chapter","created":{"date-parts":[[2023,4,16]],"date-time":"2023-04-16T20:28:25Z","timestamp":1681676905000},"page":"113-139","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Builtin Types Viewed as Inductive Families"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4091-657X","authenticated-orcid":false,"given":"Guillaume","family":"Allais","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,17]]},"reference":[{"doi-asserted-by":"publisher","unstructured":"Allais, G.: Builtin Types viewed as Inductive Families (code). University of St Andrews Research Portal (2023). https:\/\/doi.org\/10.17630\/bd1085ce-a462-4a8b-ae81-9ededb4aea21","key":"5_CR1","DOI":"10.17630\/bd1085ce-a462-4a8b-ae81-9ededb4aea21"},{"unstructured":"Allais, G., Altenm\u00fcller, M., McBride, C., Nakov, G., Forsberg, F.N., Roy, C.: TypOS: An operating system for typechecking actors. In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, Nantes, France (2022)","key":"5_CR2"},{"doi-asserted-by":"publisher","unstructured":"Altenkirch, T., McBride, C., Swierstra, W.: Observational equality, now! In: Stump, A., Xi, H. (eds.) Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007. pp. 57\u201368. ACM (2007). https:\/\/doi.org\/10.1145\/1292597.1292608","key":"5_CR3","DOI":"10.1145\/1292597.1292608"},{"doi-asserted-by":"publisher","unstructured":"Atkey, R.: Syntax and semantics of quantitative type theory. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 56\u201365. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209189","key":"5_CR4","DOI":"10.1145\/3209108.3209189"},{"doi-asserted-by":"publisher","unstructured":"Brady, E.C.: Idris 2: Quantitative type theory in practice. In: M\u00f8ller, A., Sridharan, M. (eds.) 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference). LIPIcs, vol.\u00a0194, pp. 9:1\u20139:26. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2021.9","key":"5_CR5","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"doi-asserted-by":"publisher","unstructured":"Brady, E.C., McBride, C., McKinna, J.: Inductive families need not store their indices. In: Berardi, S., Coppo, M., Damiani, F. (eds.) Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a03085, pp. 115\u2013129. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-24849-1_8","key":"5_CR6","DOI":"10.1007\/978-3-540-24849-1_8"},{"unstructured":"Brady, E.C., McKinna, J., Hammond, K.: Constructing correct circuits: Verification of functional aspects of hardware specifications with dependent types. In: Moraz\u00e1n, M.T. (ed.) Proceedings of the Eighth Symposium on Trends in Functional Programming, TFP 2007, New York City, New York, USA, April 2-4. 2007. Trends in Functional Programming, vol.\u00a08, pp. 159\u2013176. Intellect (2007)","key":"5_CR7"},{"doi-asserted-by":"publisher","unstructured":"de\u00a0Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings) 75(5), 381\u2013392 (1972). https:\/\/doi.org\/10.1016\/1385-7258(72)90034-0, https:\/\/www.sciencedirect.com\/science\/article\/pii\/1385725872900340","key":"5_CR8","DOI":"10.1016\/1385-7258(72)90034-0"},{"unstructured":"Chapman, J.M.: Type checking and normalisation. Ph.D. thesis, University of Nottingham (July 2009), http:\/\/eprints.nottingham.ac.uk\/10824\/","key":"5_CR9"},{"doi-asserted-by":"publisher","unstructured":"Cockx, J., Tabareau, N., Winterhalter, T.: The taming of the rew: a type theory with computational assumptions. Proc. ACM Program. Lang. 5(POPL), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3434341","key":"5_CR10","DOI":"10.1145\/3434341"},{"unstructured":"Coq Development\u00a0Team, T.: The Coq Proof Assistant Reference Manual, version 8.15.2 (May 2022), http:\/\/coq.inria.fr","key":"5_CR11"},{"doi-asserted-by":"publisher","unstructured":"Cornes, C., Terrasse, D.: Automating inversion of inductive predicates in coq. In: Berardi, S., Coppo, M. (eds.) Types for Proofs and Programs, International Workshop TYPES\u201995, Torino, Italy, June 5-8, 1995, Selected Papers. Lecture Notes in Computer Science, vol.\u00a01158, pp. 85\u2013104. Springer (1995). https:\/\/doi.org\/10.1007\/3-540-61780-9_64","key":"5_CR12","DOI":"10.1007\/3-540-61780-9_64"},{"doi-asserted-by":"publisher","unstructured":"Dybjer, P.: Inductive families. Formal Aspects Comput. 6(4), 440\u2013465 (1994). https:\/\/doi.org\/10.1007\/BF01211308","key":"5_CR13","DOI":"10.1007\/BF01211308"},{"doi-asserted-by":"publisher","unstructured":"Maziarz, K., Ellis, T., Lawrence, A., Fitzgibbon, A.W., Jones, S.P.: Hashing modulo alpha-equivalence. In: Freund, S.N., Yahav, E. (eds.) PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021. pp. 960\u2013973. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454088","key":"5_CR14","DOI":"10.1145\/3453483.3454088"},{"doi-asserted-by":"publisher","unstructured":"McBride, C.: Inverting inductively defined relations in LEGO. In: Gim\u00e9nez, E., Paulin-Mohring, C. (eds.) Types for Proofs and Programs, International Workshop TYPES\u201996, Aussois, France, December 15-19, 1996, Selected Papers. Lecture Notes in Computer Science, vol.\u00a01512, pp. 236\u2013253. Springer (1996). https:\/\/doi.org\/10.1007\/BFb0097795","key":"5_CR15","DOI":"10.1007\/BFb0097795"},{"doi-asserted-by":"publisher","unstructured":"McBride, C.: I got plenty o\u2019 nuttin\u2019. In: Lindley, S., McBride, C., Trinder, P.W., Sannella, D. (eds.) A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol.\u00a09600, pp. 207\u2013233. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-30936-1_12","key":"5_CR16","DOI":"10.1007\/978-3-319-30936-1_12"},{"doi-asserted-by":"publisher","unstructured":"McBride, C.: Everybody\u2019s got to be somewhere. In: Atkey, R., Lindley, S. (eds.) Proceedings of the 7th Workshop on Mathematically Structured Functional Programming, MSFP@FSCD 2018, Oxford, UK, 8th July 2018. EPTCS, vol.\u00a0275, pp. 53\u201369 (2018). https:\/\/doi.org\/10.4204\/EPTCS.275.6","key":"5_CR17","DOI":"10.4204\/EPTCS.275.6"},{"doi-asserted-by":"publisher","unstructured":"McBride, C., McKinna, J.: The view from the left. J. Funct. Program. 14(1), 69\u2013111 (2004). https:\/\/doi.org\/10.1017\/S0956796803004829","key":"5_CR18","DOI":"10.1017\/S0956796803004829"},{"unstructured":"Monin, J.F.: Proof Trick: Small Inversions. In: Bertot, Y. (ed.) Second Coq Workshop. Yves Bertot, Edinburgh, United Kingdom (Jul 2010), https:\/\/hal.inria.fr\/inria-00489412","key":"5_CR19"},{"doi-asserted-by":"publisher","unstructured":"Sozeau, M.: Equations: A dependent pattern-matching compiler. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06172, pp. 419\u2013434. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_29","key":"5_CR20","DOI":"10.1007\/978-3-642-14052-5_29"},{"doi-asserted-by":"publisher","unstructured":"Sozeau, M., Mangin, C.: Equations reloaded: high-level dependently-typed functional programming and proving in coq. Proc. ACM Program. Lang. 3(ICFP), 86:1\u201386:29 (2019). https:\/\/doi.org\/10.1145\/3341690","key":"5_CR21","DOI":"10.1145\/3341690"},{"doi-asserted-by":"publisher","unstructured":"Teji\u0161\u010d\u00e1k, M.: A dependently typed calculus with pattern matching and erasure inference. Proc. ACM Program. Lang. 4(ICFP), 91:1\u201391:29 (2020). https:\/\/doi.org\/10.1145\/3408973","key":"5_CR22","DOI":"10.1145\/3408973"},{"doi-asserted-by":"publisher","unstructured":"Vollmer, M., Koparkar, C., Rainey, M., Sakka, L., Kulkarni, M., Newton, R.R.: Local: a language for programs operating on serialized data. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019. pp. 48\u201362. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314631","key":"5_CR23","DOI":"10.1145\/3314221.3314631"},{"doi-asserted-by":"publisher","unstructured":"Wadler, P.: Views: A way for pattern matching to cohabit with data abstraction. In: Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, Munich, Germany, January 21-23, 1987. pp. 307\u2013313. ACM Press (1987). https:\/\/doi.org\/10.1145\/41625.41653","key":"5_CR24","DOI":"10.1145\/41625.41653"},{"doi-asserted-by":"publisher","unstructured":"Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad-hoc. In: Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989. pp. 60\u201376. ACM Press (1989). https:\/\/doi.org\/10.1145\/75277.75283","key":"5_CR25","DOI":"10.1145\/75277.75283"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30044-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,7]],"date-time":"2023-06-07T09:02:36Z","timestamp":1686128556000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30044-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031300431","9783031300448"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30044-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"55","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":"20","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":"36% - 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","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":"5.5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","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)"}}]}}