{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T02:07:11Z","timestamp":1781143631025,"version":"3.54.1"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004359","name":"Vetenskapsr\u00e5det","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010663","name":"European Research Council","doi-asserted-by":"publisher","award":["671500"],"award-info":[{"award-number":["671500"]}],"id":[{"id":"10.13039\/100010663","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":[[2018,1]]},"abstract":"<jats:p>\n            Linear type systems have a long and storied history, but not a clear path forward to integrate with existing languages such as OCaml or Haskell. In this paper, we study a linear type system designed with two crucial properties in mind: backwards-compatibility and code reuse across linear and non-linear users of a library. Only then can the benefits of linear types permeate conventional functional programming. Rather than bifurcate types into linear and non-linear counterparts, we instead attach linearity to\n            <jats:italic>function arrows<\/jats:italic>\n            . Linear functions can receive inputs from linearly-bound values, but can\n            <jats:italic>also<\/jats:italic>\n            operate over unrestricted, regular values.\n          <\/jats:p>\n          <jats:p>To demonstrate the efficacy of our linear type system\u00a0\u2014\u00a0both how easy it can be integrated in an existing language implementation and how streamlined it makes it to write programs with linear types\u00a0\u2014\u00a0we implemented our type system in ghc, the leading Haskell compiler, and demonstrate two kinds of applications of linear types: mutable data with pure interfaces; and enforcing protocols in I\/O-performing functions.<\/jats:p>","DOI":"10.1145\/3158093","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":80,"title":["Linear Haskell: practical linearity in a higher-order polymorphic language"],"prefix":"10.1145","volume":"2","author":[{"given":"Jean-Philippe","family":"Bernardy","sequence":"first","affiliation":[{"name":"University of Gothenburg, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mathieu","family":"Boespflug","sequence":"additional","affiliation":[{"name":"Tweag I\/O, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ryan R.","family":"Newton","sequence":"additional","affiliation":[{"name":"Indiana University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Simon","family":"Peyton Jones","sequence":"additional","affiliation":[{"name":"Microsoft Research, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Arnaud","family":"Spiwack","sequence":"additional","affiliation":[{"name":"Tweag I\/O, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_21"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Robert Atkey. 2017. The Syntax and Semantics of Quantitative Type Theory. (2017). Under submission.  Robert Atkey. 2017. The Syntax and Semantics of Quantitative Type Theory. (2017). Under submission.","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500070109"},{"key":"e_1_2_2_6_1","unstructured":"J.-P. Bernardy M. Boespflug R. R. Newton S. P. Jones and A. Spiwack. 2017. Linear Haskell: practical linearity in a higher-order polymorphic language. ArXiv e-prints (Oct. 2017). arXiv: 1710.09756  J.-P. Bernardy M. Boespflug R. R. Newton S. P. Jones and A. Spiwack. 2017. Linear Haskell: practical linearity in a higher-order polymorphic language. ArXiv e-prints (Oct. 2017). arXiv: 1710.09756"},{"key":"e_1_2_2_7_1","volume-title":"V\u00edctor L\u00f3pez Juan, and Josef Svenningsson","author":"Bernardy Jean-Philippe","year":"2015","unstructured":"Jean-Philippe Bernardy , V\u00edctor L\u00f3pez Juan, and Josef Svenningsson . 2015 . Composable Efficient Array Computations Using Linear Types. Submitted to ICFP 2015. http:\/\/www.cse.chalmers.se\/ josefs\/publications\/vectorcomp.pdf . Jean-Philippe Bernardy, V\u00edctor L\u00f3pez Juan, and Josef Svenningsson. 2015. Composable Efficient Array Computations Using Linear Types. Submitted to ICFP 2015. http:\/\/www.cse.chalmers.se\/ josefs\/publications\/vectorcomp.pdf ."},{"key":"e_1_2_2_8_1","volume-title":"Project H: Programming R in Haskell. (2014). Talk at IFL","author":"Boespflug Mathieu","year":"2014","unstructured":"Mathieu Boespflug , Facundo Dominguez , Alexander Vershilov , and Allen Brown . 2014. Project H: Programming R in Haskell. (2014). Talk at IFL 2014 . Mathieu Boespflug, Facundo Dominguez, Alexander Vershilov, and Allen Brown. 2014. Project H: Programming R in Haskell. (2014). Talk at IFL 2014."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.7494\/csci.2017.18.3.1413"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_2_2_12_1","volume-title":"Chakravarty and Gabriele Keller","author":"Manuel M.","year":"2017","unstructured":"Manuel M. T. Chakravarty and Gabriele Keller . 2017 . Haskell SpriteKit \u2013 Transforming an Imperative Object-oriented API into a Purely Functional One . (2017). http:\/\/www.cse.unsw.edu.au\/~chak\/papers\/CK17.html Manuel M. T. Chakravarty and Gabriele Keller. 2017. Haskell SpriteKit \u2013 Transforming an Imperative Object-oriented API into a Purely Functional One. (2017). http:\/\/www.cse.unsw.edu.au\/~chak\/papers\/CK17.html"},{"key":"e_1_2_2_13_1","volume-title":"Elm: Concurrent FRP for functional guis. Senior thesis","author":"Czaplicki Evan","year":"2012","unstructured":"Evan Czaplicki . 2012 . Elm: Concurrent FRP for functional guis. Senior thesis . Harvard University . Evan Czaplicki. 2012. Elm: Concurrent FRP for functional guis. Senior thesis. Harvard University."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009882"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062357"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_18_1","volume-title":"Gunter and Didier R\u00e9my","author":"Carl","year":"1993","unstructured":"Carl A. Gunter and Didier R\u00e9my . 1993 . A proof-theoretic assessment of runtime type errors. Technical Report. AT&T Bell laboratories. Technical Memo 11261-921230-43TM. Carl A. Gunter and Didier R\u00e9my. 1993. A proof-theoretic assessment of runtime type errors. Technical Report. AT&T Bell laboratories. Technical Memo 11261-921230-43TM."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411288"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018827"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2975991.2975999"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1708016.1708027"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951925"},{"key":"e_1_2_2_27_1","unstructured":"Bryan O\u2019Sullivan. 2013. The Criterion benchmarking library. http:\/\/github.com\/bos\/criterion  Bryan O\u2019Sullivan. 2013. The Criterion benchmarking library. http:\/\/github.com\/bos\/criterion"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_35"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535861"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567093"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_2_2_33_1","doi-asserted-by":"crossref","unstructured":"Jesse A Tov and Riccardo Pucella. 2011. Practical affine types. In POPL. ACM 447\u2013458.  Jesse A Tov and Riccardo Pucella. 2011. Practical affine types. In POPL. ACM 447\u2013458.","DOI":"10.1145\/1925844.1926436"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.26"},{"key":"e_1_2_2_35_1","volume-title":"Linear types can change the world","author":"Wadler Philip","unstructured":"Philip Wadler . 1990. Linear types can change the world . In Programming Concepts and Methods, M Broy and C B Jones (Eds.). North-Holland . Philip Wadler. 1990. Linear types can change the world. In Programming Concepts and Methods, M Broy and C B Jones (Eds.). North-Holland."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110275"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30557-6_8"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158093","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158093","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158093"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":36,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158093"],"URL":"https:\/\/doi.org\/10.1145\/3158093","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}