{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:14:14Z","timestamp":1767928454392,"version":"3.49.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,8,29]]},"abstract":"<jats:p>A linear parameter must be consumed exactly once in the body of its function. When declaring resources such as file handles and manually managed memory as linear arguments, a linear type system can verify that these resources are used safely. However, writing code with explicit linear arguments requires bureaucracy. This paper presents linear constraints, a front-end feature for linear typing that decreases the bureaucracy of working with linear types. Linear constraints are implicit linear arguments that are filled in automatically by the compiler. We present linear constraints as a qualified type system,together with an inference algorithm which extends GHC's existing constraint solver algorithm. Soundness of linear constraints is ensured by the fact that they desugar into Linear Haskell.<\/jats:p>","DOI":"10.1145\/3547626","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"137-164","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Linearly qualified types: generic inference for capabilities and uniqueness"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5985-2086","authenticated-orcid":false,"given":"Arnaud","family":"Spiwack","sequence":"first","affiliation":[{"name":"Tweag, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0195-2420","authenticated-orcid":false,"given":"Csongor","family":"Kiss","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8469-5617","authenticated-orcid":false,"given":"Jean-Philippe","family":"Bernardy","sequence":"additional","affiliation":[{"name":"University of Gothenburg, Sweden"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4161-985X","authenticated-orcid":false,"given":"Nicolas","family":"Wu","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7669-9781","authenticated-orcid":false,"given":"Richard A.","family":"Eisenberg","sequence":"additional","affiliation":[{"name":"Tweag, France"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408972"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122967"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00173-5"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292564"},{"key":"e_1_2_1_6_1","volume-title":"Jean Baptiste Joinet, and Harold Schellinx","author":"Danos Vincent","year":"1993","unstructured":"Vincent Danos , Jean Baptiste Joinet, and Harold Schellinx . 1993 . The structure of exponentials: Uncovering the dynamics of linear logic proofs. In Computational Logic and Proof Theory, Georg Gottlob, Alexander Leitsch, and Daniele Mundici (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 159\u2013171. isbn:978-3-540-47943-7 Vincent Danos, Jean Baptiste Joinet, and Harold Schellinx. 1993. The structure of exponentials: Uncovering the dynamics of linear logic proofs. In Computational Logic and Proof Theory, Georg Gottlob, Alexander Leitsch, and Daniele Mundici (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 159\u2013171. isbn:978-3-540-47943-7"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"e_1_2_1_8_1","unstructured":"Facundo Dom\u00ednguez. 2020. Safe memory management in inline-java using linear types. https:\/\/web.archive.org\/web\/20200926082552\/https:\/\/www.tweag.io\/blog\/2020-02-06-safe-inline-java\/ Blog post \t\t\t\t  Facundo Dom\u00ednguez. 2020. Safe memory management in inline-java using linear types. https:\/\/web.archive.org\/web\/20200926082552\/https:\/\/www.tweag.io\/blog\/2020-02-06-safe-inline-java\/ Blog post"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473569"},{"key":"e_1_2_1_10_1","volume-title":"Ahmed","author":"Eisenberg Richard A.","year":"2016","unstructured":"Richard A. Eisenberg , Stephanie Weirich , and Hamidhasan G . Ahmed . 2016 . Visible Type Application. In Programming Languages and Systems, Peter Thiemann (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg. 229\u2013254. isbn:978-3-662-49498-1 Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed. 2016. Visible Type Application. In Programming Languages and Systems, Peter Thiemann (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 229\u2013254. isbn:978-3-662-49498-1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_2"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/227699.227700"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1036"},{"key":"e_1_2_1_15_1","unstructured":"Joshua Seth Hodas. 1994. Logic programming in intuitionistic linear logic: Theory design and implementation. https:\/\/repository.upenn.edu\/dissertations\/AAI9427546 \t\t\t\t  Joshua Seth Hodas. 1994. Logic programming in intuitionistic linear logic: Theory design and implementation. https:\/\/repository.upenn.edu\/dissertations\/AAI9427546"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00005-0"},{"key":"e_1_2_1_17_1","volume-title":"Eisenberg","author":"Kiss Csongor","year":"2022","unstructured":"Csongor Kiss , Arnaud Spiwack , Jean-Philippe Bernardy , Nicolas Wu , and Richard A . Eisenberg . 2022 . Prototype implementation of linear constraints in GHC. http:\/\/archive.softwareheritage.org\/swh:1:rev:f6fc5ba23770b42d1d6020e177787757b16a9ea0;origin=https:\/\/github.com\/kcsongor\/ghc;visit=swh:1:snp:aa61d803eaec9eb4425e3eb8ed2b0fbbd60633cc Code fragment Csongor Kiss, Arnaud Spiwack, Jean-Philippe Bernardy, Nicolas Wu, and Richard A. Eisenberg. 2022. Prototype implementation of linear constraints in GHC. http:\/\/archive.softwareheritage.org\/swh:1:rev:f6fc5ba23770b42d1d6020e177787757b16a9ea0;origin=https:\/\/github.com\/kcsongor\/ghc;visit=swh:1:snp:aa61d803eaec9eb4425e3eb8ed2b0fbbd60633cc Code fragment"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/330249.330251"},{"key":"e_1_2_1_19_1","volume-title":"Modular Inference of Linear Types for Multiplicity-Annotated Arrows","author":"Matsuda Kazutaka","unstructured":"Kazutaka Matsuda . 2020. Modular Inference of Linear Types for Multiplicity-Annotated Arrows . In Programming Languages and Systems, Peter M\u00fcller (Ed.). Springer International Publishing , Cham . 456\u2013483. isbn:978-3-030-44914-8 Kazutaka Matsuda. 2020. Modular Inference of Linear Types for Multiplicity-Annotated Arrows. In Programming Languages and Systems, Peter M\u00fcller (Ed.). Springer International Publishing, Cham. 456\u2013483. isbn:978-3-030-44914-8"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS","author":"Miller Dale A.","year":"1987","unstructured":"Dale A. Miller , Gopalan Nadathur , and Andre Scedrov . 1987 . Hereditary Harrop Formulas and Uniform Proof Systems . In Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987). IEEE Computer Society Press, 98\u2013105. Dale A. Miller, Gopalan Nadathur, and Andre Scedrov. 1987. Hereditary Harrop Formulas and Uniform Proof Systems. In Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987). IEEE Computer Society Press, 98\u2013105."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"e_1_2_1_22_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2002. Types and Programming Languages . MIT Press, Cambridge , MA. Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, MA."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500598"},{"key":"e_1_2_1_24_1","unstructured":"Fran\u00e7ois Pottier and Didier R\u00e9my. 2005. The essence of ML type inference. \t\t\t\t  Fran\u00e7ois Pottier and Didier R\u00e9my. 2005. The essence of ML type inference."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408985"},{"key":"e_1_2_1_26_1","unstructured":"Michael Shulman. 2018. Linear logic for constructive mathematics. arxiv:1805.07518. \t\t\t\t  Michael Shulman. 2018. Linear logic for constructive mathematics. arxiv:1805.07518."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46425-5_24"},{"key":"e_1_2_1_28_1","volume-title":"Eisenberg","author":"Spiwack Arnaud","year":"2021","unstructured":"Arnaud Spiwack , Csongor Kiss , Jean-Philippe Bernardy , Nicolas Wu , and Richard A . Eisenberg . 2021 . Linear Constraints. CoRR , abs\/2103.06127 (2021), arXiv:2103.06127. arxiv:2103.06127 Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, and Richard A. Eisenberg. 2021. Linear Constraints. CoRR, abs\/2103.06127 (2021), arXiv:2103.06127. arxiv:2103.06127"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1708016.1708023"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45332-6_7"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110275"},{"key":"e_1_2_1_34_1","volume-title":"Practical Aspects of Declarative Languages, Manuel V","author":"Zhu Dengping","unstructured":"Dengping Zhu and Hongwei Xi. 2005. Safe Programming with Pointers Through Stateful Views . In Practical Aspects of Declarative Languages, Manuel V . Hermenegildo and Daniel Cabeza (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 83\u201397. isbn:978-3-540-30557-6 Dengping Zhu and Hongwei Xi. 2005. Safe Programming with Pointers Through Stateful Views. In Practical Aspects of Declarative Languages, Manuel V. Hermenegildo and Daniel Cabeza (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 83\u201397. isbn:978-3-540-30557-6"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547626","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547626","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:28Z","timestamp":1750272208000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547626"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":34,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547626"],"URL":"https:\/\/doi.org\/10.1145\/3547626","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}