{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:59Z","timestamp":1775873699668,"version":"3.50.1"},"reference-count":80,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T00:00:00Z","timestamp":1693353600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP19K11892, JP20H04161, JP22H03562"],"award-info":[{"award-number":["JP19K11892, JP20H04161, JP22H03562"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000288","name":"Royal Society","doi-asserted-by":"publisher","award":["IES\\R3\\170104"],"award-info":[{"award-number":["IES\\R3\\170104"]}],"id":[{"id":"10.13039\/501100000288","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/T008911\/1"],"award-info":[{"award-number":["EP\/T008911\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,8,30]]},"abstract":"<jats:p>\n            Embedding is a language development technique that implements the object language as a library in a host language.  \nThere are many advantages of the approach, including being lightweight and the ability to inherit features of the host language. A notable example is the technique of HOAS, which makes crucial use of higher-order functions to represent abstract syntax trees with binders.  \nDespite its popularity, HOAS has its limitations.  \nWe observe that HOAS struggles with semantic domains that cannot be naturally expressed as functions, particularly when open expressions are involved.  \nProminent examples of this include incremental computation and reversible\/bidirectional languages.  \n  \nIn this paper, we pin-point the challenge faced by HOAS as a mismatch between the semantic domain of host and object language functions, and propose a solution.  \nThe solution is based on the technique of\n            <jats:italic>unembedding<\/jats:italic>\n            , which converts  \nfrom the finally-tagless representation to de Bruijn-indexed terms with  \nstrong correctness guarantees. We show that this approach is able to extend the  \napplicability of HOAS while preserving its elegance. We provide a generic  \nstrategy for Embedding by Unembedding, and then demonstrate its effectiveness  \nwith two substantial case studies in the domains of incremental computation  \nand bidirectional transformations. The resulting embedded implementations are  \ncomparable in features to the state-of-the-art language implementations in  \nthe respective areas.\n          <\/jats:p>","DOI":"10.1145\/3607830","type":"journal-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:40:31Z","timestamp":1693503631000},"page":"1-47","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Embedding by Unembedding"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9747-4899","authenticated-orcid":false,"given":"Kazutaka","family":"Matsuda","sequence":"first","affiliation":[{"name":"Tohoku University, Japan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4423-6918","authenticated-orcid":false,"given":"Samantha","family":"Frohlich","sequence":"additional","affiliation":[{"name":"University of Bristol, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7780-630X","authenticated-orcid":false,"given":"Meng","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Bristol, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4161-985X","authenticated-orcid":false,"given":"Nicolas","family":"Wu","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]}],"member":"320","published-online":{"date-parts":[[2023,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.002"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1186632.1186634"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429376.2429382"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_5"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596638.1596644"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/319628.319634"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_2_1_8_1","volume-title":"Tensor Partial Evaluation. HOPE 2021: The 8th ACM SIGPLAN Workshop on Higher-Order Programming with Effects. Extend Abstract Avaiable via: https:\/\/icfp21","author":"Bingham Eli","year":"2021","unstructured":"Eli Bingham, Fritz Obermeyer, Yerdos Ordabayev, and Du Phan. 2021. Tensor Partial Evaluation. HOPE 2021: The 8th ACM SIGPLAN Workshop on Higher-Order Programming with Effects. Extend Abstract Avaiable via: https:\/\/icfp21.sigplan.org\/details\/hope-2021-papers\/4\/Tensor-Partial-Evaluation"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594304"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007205"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434290"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254100"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000033"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000033"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/154630.154643"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00392-X"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110271"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2010.5447896"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237792"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_19"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15205-4_26"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782615"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040325"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1232420.1232424"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_20"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628138"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165214"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-90686-7_7"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000157"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542480"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-53507-1_93"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026193328134"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264598"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45231-5_17"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.294.2"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017488"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498710"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_6"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784750"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000096"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242758"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00354-018-0033-7"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_2"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409000"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434309"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500595"},{"key":"e_1_2_1_50_1","volume-title":"Embedded Pattern Matching. CoRR, abs\/2108.13114","author":"McDonell Trevor L.","year":"2021","unstructured":"Trevor L. McDonell, Joshua D. Meredith, and Gabriele Keller. 2021. Embedded Pattern Matching. CoRR, abs\/2108.13114 (2021), arXiv:2108.13114. arxiv:2108.13114"},{"key":"e_1_2_1_51_1","first-page":"0799","volume-title":"Proceedings of the 1987 Symposium on Logic Programming","author":"Miller Dale","year":"1987","unstructured":"Dale Miller and Gopalan Nadathur. 1987. A Logic Programming Approach to Manipulating Formulas and Programs. In Proceedings of the 1987 Symposium on Logic Programming, San Francisco, California, USA, August 31 - September 4, 1987. IEEE-CS, 379\u2013388. isbn:0-8186-0799-8"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158089"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053552"},{"key":"e_1_2_1_54_1","unstructured":"Akimasa Morihata. 2020. Short Cut to Incremental Typed Functional Programs. Informal Proceedings of WPTE 2020: 7th International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Available from http:\/\/maude.ucm.es\/wpte20\/papers\/WPTE_2020_morihata.pdf"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","unstructured":"Minh Nguyen Roly Perera Meng Wang and Steven Ramsay. 2023. Effect handlers for programmable inference. https:\/\/doi.org\/10.1145\/3609026.3609729","DOI":"10.1145\/3609026.3609729"},{"key":"e_1_2_1_56_1","volume-title":"Chen","author":"Obermeyer Fritz","year":"2020","unstructured":"Fritz Obermeyer, Eli Bingham, Martin Jankowiak, Du Phan, and Jonathan P. Chen. 2020. Functional Tensors for Probabilistic Programming. arxiv:1910.10775."},{"key":"e_1_2_1_57_1","volume-title":"Mathematics of Program Construction, Claude Bolduc, Jules Desharnais, and B\u00e9chir Ktari (Eds.)","author":"Pacheco Hugo","unstructured":"Hugo Pacheco and Alcino Cunha. 2010. Generic Point-free Lenses. In Mathematics of Program Construction, Claude Bolduc, Jules Desharnais, and B\u00e9chir Ktari (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 331\u2013352. isbn:978-3-642-13321-3"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804316"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328483"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804309"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.14279\/tuj.eceasst.57.879"},{"key":"e_1_2_1_63_1","unstructured":"John C. Reynolds. 1983. Types Abstraction and Parametric Polymorphism. In Information Processing R.E.A. Mason (Ed.). Elsevier Science Publishers B.V. (North-Holland) 513\u2013523."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273442.1250770"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/636517.636528"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434284"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88643-3_10"},{"key":"e_1_2_1_68_1","unstructured":"Don Stewart. 2010. yices-painless: An embedded language for programming the Yices SMT solver. In Hackage:. https:\/\/hackage.haskell.org\/package\/yices-painless Visited 2022-06-27"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.14778\/3377369.3377380"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480904"},{"key":"e_1_2_1_71_1","unstructured":"Dimitrios Vytiniotis Dan Belov Richard Wei Gordon Plotkin and Martin Abadi. 2019. The Differentiable Curry. Program Transformations for Machine Learning@NeurIPS. Availble from: https:\/\/openreview.net\/pdf?id=ryxuz9SzDB"},{"key":"e_1_2_1_72_1","doi-asserted-by":"crossref","unstructured":"Philip Wadler. 1989. Theorems for Free!. In FPCA. 347\u2013359.","DOI":"10.1145\/99370.99404"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317794"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341700"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13321-3_22"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2012.07.014"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364474.2364488"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321657"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29517-1_2"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227162"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607830","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607830","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:05Z","timestamp":1750178225000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607830"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,30]]},"references-count":80,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2023,8,30]]}},"alternative-id":["10.1145\/3607830"],"URL":"https:\/\/doi.org\/10.1145\/3607830","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,8,30]]},"assertion":[{"value":"2023-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}