{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:13:34Z","timestamp":1775873614367,"version":"3.50.1"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T00:00:00Z","timestamp":1723680000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100004063","name":"Knut and Alice Wallenberg Foundation","doi-asserted-by":"crossref","award":["2019.0116"],"award-info":[{"award-number":["2019.0116"]}],"id":[{"id":"10.13039\/501100004063","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,8,15]]},"abstract":"<jats:p>Many abstraction tools in functional programming rely heavily on general-purpose compiler optimization to achieve adequate performance. For example, monadic binding is a higher-order function which yields runtime closures in the absence of sufficient compile-time inlining and beta-reductions, thereby significantly degrading performance. In current systems such as the Glasgow Haskell Compiler, there is no strong guarantee that general-purpose optimization can eliminate abstraction overheads, and users only have indirect and fragile control over code generation through inlining directives and compiler options. We propose a two-stage language to simultaneously get strong guarantees about code generation and strong abstraction features. The object language is a simply-typed first-order language which can be compiled without runtime closures. The compile-time language is a dependent type theory. The two are integrated in a two-level type theory.<\/jats:p>\n                  <jats:p>We demonstrate two applications of the system. First, we develop monads and monad transformers. Here, abstraction overheads are eliminated by staging and we can reuse almost all definitions from the existing Haskell ecosystem. Second, we develop pull-based stream fusion. Here we make essential use of dependent types to give a concise definition of a concatMap operation with guaranteed fusion. We provide an Agda implementation and a typed Template Haskell implementation of these developments.<\/jats:p>","DOI":"10.1145\/3674648","type":"journal-article","created":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T12:49:04Z","timestamp":1723726144000},"page":"659-692","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Closure-Free Functional Programming in a Two-Level Type Theory"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6375-9781","authenticated-orcid":false,"given":"Andr\u00e1s","family":"Kov\u00e1cs","sequence":"first","affiliation":[{"name":"University of Gothenburg, Gothenburg, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,8,15]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"Agda developers. 2024. Agda documentation. https:\/\/agda.readthedocs.io\/en\/v2.6.4.2\/"},{"key":"e_1_3_1_3_1","article-title":"Two-Level Type Theory and Applications","author":"Annenkov Danil","year":"2019","unstructured":"Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. 2019. Two-Level Type Theory and Applications. ArXiv e-prints (may 2019). http:\/\/arxiv.org\/abs\/1705.03307","journal-title":"ArXiv e-prints"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141483"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-14675-1_3"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2008.09.008"},{"key":"e_1_3_1_8_1","volume-title":"Generalised algebraic theories and contextual categories","author":"Cartmell John","year":"1978","unstructured":"John Cartmell. 1978. Generalised algebraic theories and contextual categories. Ph. D. Dissertation. Oxford University."},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926397"},{"key":"e_1_3_1_10_1","volume-title":"Stream fusion : practical shortcut fusion for coinductive sequence types","author":"Coutts Duncan","year":"2011","unstructured":"Duncan Coutts. 2011. Stream fusion : practical shortcut fusion for coinductive sequence types. Ph. D. Dissertation. University of Oxford, UK. http:\/\/ora.ox.ac.uk\/objects\/uuid:b4971f57-2b94-4fdf-a5c0-98d6935a44da"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/236114.236119"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/773184.773202"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633628.2633634"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633628.2633634"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408986"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364522"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_3_1_20_1","unstructured":"GHC developers. 2024a. GHC documentation. https:\/\/downloads.haskell.org\/ghc\/9.8.2\/docs\/users_guide\/"},{"key":"e_1_3_1_21_1","unstructured":"GHC developers. 2024a. GHC.Base source. https:\/\/hackage.haskell.org\/package\/base-4.19.1.0\/docs\/src\/GHC.Base.html#."},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24276-2_2"},{"key":"e_1_3_1_24_1","doi-asserted-by":"crossref","unstructured":"Martin Hofmann. 1995. Conservativity of Equality Reflection over Intensional Type Theory.. In TYPES 95. 153\u2013164.","DOI":"10.1007\/3-540-61780-9_68"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.004"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782616"},{"key":"e_1_3_1_27_1","volume-title":"Cubical Interpretations of Type Theory","author":"Huber Simon","year":"2016","unstructured":"Simon Huber. 2016. Cubical Interpretations of Type Theory. Ph. D. Dissertation. University of Gothenburg."},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2020.8"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/153676"},{"key":"e_1_3_1_30_1","first-page":"47","article-title":"Tackling the awkward squad: monadic input\/output, concurrency, exceptions, and foreign-language calls in Haskell","volume":"180","author":"Jones Simon Peyton","year":"2001","unstructured":"Simon Peyton Jones. 2001. Tackling the awkward squad: monadic input\/output, concurrency, exceptions, and foreign-language calls in Haskell. NATO SCIENCE SERIES SUB SERIES III COMPUTER AND SYSTEMS SCIENCES 180 (2001), 47\u201396.","journal-title":"NATO SCIENCE SERIES SUB SERIES III COMPUTER AND SYSTEMS SCIENCES"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009880"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017753.1017794"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3635800.3636962"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547641"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","unstructured":"Andr\u00e1s Kov\u00e1cs. 2023. Type-Theoretic Signatures for Algebraic Theories and Inductive Types. CoRR abs\/2302.08837 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2302.08837 10.48550\/ARXIV.2302.08837 arXiv:2302.08837","DOI":"10.48550\/ARXIV.2302.08837"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","unstructured":"Andr\u00e1s Kov\u00e1cs. 2022. Demo implementation for the paper \u201cStaged Compilation With Two-Level Type Theory\u201d. https:\/\/doi.org\/10.5281\/zenodo.6757373 10.5281\/zenodo.6757373","DOI":"10.5281\/zenodo.6757373"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","unstructured":"Andr\u00e1s Kov\u00e1cs. 2024. Artifacts for the paper \u201cClosure-Free Functional Programming in a Two-Level Type Theory\u201d. https:\/\/doi.org\/10.5281\/zenodo.12656335 10.5281\/zenodo.12656335","DOI":"10.5281\/zenodo.12656335"},{"key":"e_1_3_1_38_1","unstructured":"Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my KC Sivaramakrishnan and J\u00e9r\u00f4me Vouillon. 2023. The OCaml system release 5.1: Documentation and user\u2019s manual. https:\/\/v2.ocaml.org\/manual\/"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_17"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062380"},{"key":"e_1_3_1_42_1","unstructured":"mtl developers. 2024. mtl documentation. https:\/\/hackage.haskell.org\/package\/mtl"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_3_1_44_1","volume-title":"Abstract interpretation using domain theory","author":"Nielson Flemming","year":"1984","unstructured":"Flemming Nielson. 1984. Abstract interpretation using domain theory. Ph. D. Dissertation. University of Edinburgh, UK. https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.350060"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526572"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3406088.3409021"},{"key":"e_1_3_1_47_1","unstructured":"Brigitte Pientka Andreas Abel Francisco Ferreira David Thibodeau and R\u00e9becca Zucchini. 2019. Cocon: Computation in Contextual Type Theory. CoRR abs\/1901.03378 (2019). arXiv:1901.03378 http:\/\/arxiv.org\/abs\/1901.03378"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010027404223"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3131851.3131865"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2184319.2184345"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111542.1111570"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","unstructured":"Walid Taha and Tim Sheard. 2000. MetaML and multi-stage programming with explicit annotations. Theor. Comput. Sci. 248 1\u20132 (2000) 211\u2013242. https:\/\/doi.org\/10.1016\/S0304-3975(00)00053-0 10.1016\/S0304-3975(00)00053-0","DOI":"10.1016\/S0304-3975(00)00053-0"},{"key":"e_1_3_1_53_1","unstructured":"Vladimir Voevodsky. 2013. A simple type system with two identity types. (2013). Unpublished note."},{"key":"e_1_3_1_54_1","first-page":"347","volume-title":"Functional Programming Languages and Computer Architecture","author":"Wadler Philip","year":"1989","unstructured":"Philip Wadler. 1989. Theorems for free!. In Functional Programming Languages and Computer Architecture. ACM Press, 347\u2013359."},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498723"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3294032.3294078"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674648","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3674648","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:49:27Z","timestamp":1770191367000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674648"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,15]]},"references-count":56,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2024,8,15]]}},"alternative-id":["10.1145\/3674648"],"URL":"https:\/\/doi.org\/10.1145\/3674648","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,15]]},"assertion":[{"value":"2024-02-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}