{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:01Z","timestamp":1751660521390,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T00:00:00Z","timestamp":1540339200000},"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":[[2018,10,24]]},"abstract":"<jats:p>Refinement types allow for lightweight program verification by enriching types with logical predicates. Liquid typing provides a decidable refinement inference mechanism that is convenient but subject to two major issues: (1) inference is global and requires top-level annotations, making it unsuitable for inference of modular code components and prohibiting its applicability to library code, and (2) inference failure results in obscure error messages. These difficulties seriously hamper the migration of existing code to use refinements.<\/jats:p>\n          <jats:p>\n            This paper shows that\n            <jats:italic>gradual liquid type inference<\/jats:italic>\n            \u2013a novel combination of liquid inference and gradual refinement types\u2013addresses both issues. Gradual refinement types, which support imprecise predicates that are optimistically interpreted, can be used in argument positions to constrain liquid inference so that the global inference process effectively infers modular specifications usable for library components. Dually, when gradual refinements appear as the result of inference, they signal an inconsistency in the use of static refinements. Because liquid refinements are drawn from a finite set of predicates, in gradual liquid type inference we can enumerate the textitsafe concretizations of each imprecise refinement,\n            <jats:italic>i.e.,<\/jats:italic>\n            the static refinements that justify why a program is gradually well-typed. This enumeration is useful for static liquid type error explanation, since the safe concretizations exhibit all the potential inconsistencies that lead to static type errors.\n          <\/jats:p>\n          <jats:p>We develop the theory of gradual liquid type inference and explore its pragmatics in the setting of Liquid Haskell. To demonstrate the utility of our approach, we develop an interactive tool, GuiLT, for gradual liquid type inference in Liquid Haskell that both infers modular types and explores safe concretizations of gradual refinements. We report on the use of GuiLT for error reporting and discuss a case study on the migration of three commonly-used Haskell list manipulation libraries into Liquid Haskell.<\/jats:p>","DOI":"10.1145\/3276502","type":"journal-article","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T11:57:18Z","timestamp":1540382238000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Gradual liquid type inference"],"prefix":"10.1145","volume":"2","author":[{"given":"Niki","family":"Vazou","sequence":"first","affiliation":[{"name":"IMDEA Software Institute, Spain"}]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Chile"}]},{"given":"David","family":"Van Horn","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]}],"member":"320","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"volume-title":"Coq\u2019Art: The Calculus of Inductive Constructions","author":"Bertot Yves","key":"e_1_2_2_1_1","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . 2004. Coq\u2019Art: The Calculus of Inductive Constructions . Springer Verlag . Yves Bertot and Pierre Cast\u00e9ran. 2004. Coq\u2019Art: The Calculus of Inductive Constructions. Springer Verlag."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158103"},{"key":"e_1_2_2_3_1","doi-asserted-by":"crossref","unstructured":"Sheng Chen and Martin Erwig. 2018. Systematic identification and communication of type errors. JFP 28.  Sheng Chen and Martin Erwig. 2018. Systematic identification and communication of type errors. JFP 28.","DOI":"10.1017\/S095679681700020X"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2518190"},{"volume-title":"Courcelle and Joost Engelfriet","year":"2012","key":"e_1_2_2_5_1","unstructured":"Bruno. Courcelle and Joost Engelfriet . 2012 . Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach (1st ed.). Cambridge University Press . Bruno. Courcelle and Joost Engelfriet. 2012. Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach (1st ed.). Cambridge University Press."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676992"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706341"},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Christian Haack and Joe Wells. 2003. Type Error Slicing in Implicitly-Typed Higher-Order Languages. In ESOP.   Christian Haack and Joe Wells. 2003. Type Error Slicing in Implicitly-Typed Higher-Order Languages. In ESOP.","DOI":"10.1007\/3-540-36575-3_20"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009856"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250783"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737971"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628156"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158139"},{"volume-title":"Jean-Jacques Levy, Ernst W","author":"Ou Xinming","key":"e_1_2_2_17_1","unstructured":"Xinming Ou , Gang Tan , Yitzhak Mandelbaum , and David Walker . 2004. Dynamic Typing with Dependent Types , Jean-Jacques Levy, Ernst W . Mayr, and John C. Mitchell (Eds.). IFIP. Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. 2004. Dynamic Typing with Dependent Types, Jean-Jacques Levy, Ernst W. Mayr, and John C. Mitchell (Eds.). IFIP."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660230"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103714"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951915"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3138818"},{"key":"e_1_2_2_23_1","volume-title":"Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop.","author":"Siek Jeremy","year":"2006","unstructured":"Jeremy Siek and Walid Taha . 2006 . Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop. Jeremy Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1408681.1408688"},{"key":"e_1_2_2_25_1","unstructured":"Jeremy G. Siek Michael M. Vitousek Matteo Cimini and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In SNAPL.  Jeremy G. Siek Michael M. Vitousek Matteo Cimini and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In SNAPL."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/366378.366379"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384655"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_2_32_1","volume-title":"Gradual Liquid Types. ArXiv e-prints","author":"Vazou Niki","year":"2018","unstructured":"Niki Vazou , \u00c9ric Tanter , and David Van Horn . 2018a. Gradual Liquid Types. ArXiv e-prints ( 2018 ). arXiv: 1807.02132 Niki Vazou, \u00c9ric Tanter, and David Van Horn. 2018a. Gradual Liquid Types. ArXiv e-prints (2018). arXiv: 1807.02132"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512648"},{"key":"e_1_2_2_35_1","unstructured":"Makarius Wenzel. 2016. The Isabelle System Manual. (2016). https:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/dist\/ Isabelle2016- 1\/doc\/system.pdf  Makarius Wenzel. 2016. The Isabelle System Manual. (2016). https:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/dist\/ Isabelle2016- 1\/doc\/system.pdf"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738009"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276502","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276502","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:03:39Z","timestamp":1750273419000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276502"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,24]]},"references-count":36,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2018,10,24]]}},"alternative-id":["10.1145\/3276502"],"URL":"https:\/\/doi.org\/10.1145\/3276502","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2018,10,24]]},"assertion":[{"value":"2018-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}