{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T04:20:57Z","timestamp":1752985257787,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003802","name":"University Research Committee, University of Hong Kong","doi-asserted-by":"publisher","award":["17210617, 17258816"],"award-info":[{"award-number":["17210617, 17258816"]}],"id":[{"id":"10.13039\/501100003802","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003130","name":"Fonds Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003130","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":[[2019,7,26]]},"abstract":"<jats:p>Elaboration-based type class resolution, as found in languages like Haskell, Mercury and PureScript, is generally nondeterministic: there can be multiple ways to satisfy a wanted constraint in terms of global instances and locally given constraints. Coherence is the key property that keeps this sane; it guarantees that, despite the nondeterminism, programs still behave predictably. Even though elaboration-based resolution is generally assumed coherent, as far as we know, there is no formal proof of this property in the presence of sources of nondeterminism, like superclasses and flexible contexts.<\/jats:p>\n          <jats:p>This paper provides a formal proof to remedy the situation. The proof is non-trivial because the semantics elaborates resolution into a target language where different elaborations can be distinguished by contexts that do not have a source language counterpart. Inspired by the notion of full abstraction, we present a two-step strategy that first elaborates nondeterministically into an intermediate language that preserves contextual equivalence, and then deterministically elaborates from there into the target language. We use an approach based on logical relations to establish contextual equivalence and thus coherence for the first step of elaboration, while the second step\u2019s determinism straightforwardly preserves this coherence property.<\/jats:p>","DOI":"10.1145\/3341695","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Coherence of type class resolution"],"prefix":"10.1145","volume":"3","author":[{"given":"Gert-Jan","family":"Bottu","sequence":"first","affiliation":[{"name":"KU Leuven, Belgium"}]},{"given":"Ningning","family":"Xie","sequence":"additional","affiliation":[{"name":"University of Hong Kong, China"}]},{"given":"Koar","family":"Marntirosian","sequence":"additional","affiliation":[{"name":"KU Leuven, Belgium"}]},{"given":"Tom","family":"Schrijvers","sequence":"additional","affiliation":[{"name":"KU Leuven, Belgium"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"volume-title":"Protection in Programming-Language Translations","author":"Abadi Mart\u00edn","key":"e_1_2_2_1_1","unstructured":"Mart\u00edn Abadi . 1999. Protection in Programming-Language Translations . Springer , 19\u201334. Mart\u00edn Abadi. 1999. Protection in Programming-Language Translations. Springer, 19\u201334."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_2_3_1","unstructured":"Amal Ahmed. 2015. Logical Relations. https:\/\/www.cs.uoregon.edu\/research\/summerschool\/summer15\/curriculum.html .  Amal Ahmed. 2015. Logical Relations. https:\/\/www.cs.uoregon.edu\/research\/summerschool\/summer15\/curriculum.html ."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_2_2_5_1","volume-title":"d. S. Oliveira, and Tom Schrijvers","author":"Bi Xuan","year":"2018","unstructured":"Xuan Bi , Bruno C. d. S. Oliveira, and Tom Schrijvers . 2018 . The essence of nested composition. In ECOOP. Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2018. The essence of nested composition. In ECOOP."},{"key":"e_1_2_2_6_1","volume-title":"d. S. Oliveira, and Tom Schrijvers","author":"Bi Xuan","year":"2019","unstructured":"Xuan Bi , Ningning Xie , Bruno C. d. S. Oliveira, and Tom Schrijvers . 2019 . Distributive Disjoint Polymorphism for Compositional Programming . (2019). Xuan Bi, Ningning Xie, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. Distributive Disjoint Polymorphism for Compositional Programming. (2019)."},{"key":"e_1_2_2_7_1","unstructured":"Dariusz Biernacki and Piotr Polesiuk. 2015. Logical relations for coherence of effect subtyping. In LIPIcs.  Dariusz Biernacki and Piotr Polesiuk. 2015. Logical relations for coherence of effect subtyping. In LIPIcs."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122967"},{"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.1145\/1090189.1086397"},{"key":"e_1_2_2_11_1","volume-title":"Floris Van Doorn, and Jakob von Raumer","author":"de Moura Leonardo","year":"2015","unstructured":"Leonardo de Moura , Soonho Kong , Jeremy Avigad , Floris Van Doorn, and Jakob von Raumer . 2015 . The Lean theorem prover. (2015). Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. 2015. The Lean theorem prover. (2015)."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034796"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190229"},{"key":"e_1_2_2_14_1","unstructured":"Phil Freeman. 2017. PureScript by Example. Leanpub. https:\/\/leanpub.com\/purescript .  Phil Freeman. 2017. PureScript by Example. Leanpub. https:\/\/leanpub.com\/purescript ."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1167515.1167499"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/227699.227700"},{"key":"e_1_2_2_18_1","volume-title":"Practical Foundations for Programming Languages","author":"Harper Robert","unstructured":"Robert Harper . 2016. Practical Foundations for Programming Languages ( 2 nd ed.). Cambridge University Press . Robert Harper. 2016. Practical Foundations for Programming Languages (2nd ed.). Cambridge University Press.","edition":"2"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663086"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/645394.651909"},{"key":"e_1_2_2_23_1","volume-title":"Proc. Haskell Workshop","volume":"59","author":"Kahl Wolfram","year":"2001","unstructured":"Wolfram Kahl and Jan Scheffczyk . 2001 . Named Instances for Haskell Type Classes . In Proc. Haskell Workshop 2001, Ralf Hinze (Ed.) , Vol. 59 . Wolfram Kahl and Jan Scheffczyk. 2001. Named Instances for Haskell Type Classes. In Proc. Haskell Workshop 2001, Ralf Hinze (Ed.), Vol. 59."},{"key":"e_1_2_2_24_1","volume-title":"Pierce","author":"Lampropoulos Leonidas","year":"2018","unstructured":"Leonidas Lampropoulos and Benjamin C . Pierce . 2018 . QuickChick: Property- Based Testing in Coq (1st ed.). Software Foundations , Vol. 4 . Leonidas Lampropoulos and Benjamin C. Pierce. 2018. QuickChick: Property-Based Testing in Coq (1st ed.). Software Foundations, Vol. 4."},{"key":"e_1_2_2_25_1","unstructured":"Lex Spoon Martin Odersky and Bill Venners. 2008. Implicit Conversions and Parameters. In Programming in Scala. Chapter 21.  Lex Spoon Martin Odersky and Bill Venners. 2008. Implicit Conversions and Parameters. In Programming in Scala. Chapter 21."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633364"},{"key":"e_1_2_2_28_1","unstructured":"Team Mozilla Research. 2017. The Rust Programming Language. https:\/\/www.rust- lang.org\/en- US\/ .  Team Mozilla Research. 2017. The Rust Programming Language. https:\/\/www.rust- lang.org\/en- US\/ ."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158130"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_6"},{"volume-title":"Haskell 98 Language and Libraries: The Revised Report","author":"Jones Simon Peyton","key":"e_1_2_2_31_1","unstructured":"Simon Peyton Jones . 2003. Haskell 98 Language and Libraries: The Revised Report . Cambridge University Press . Simon Peyton Jones. 2003. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_2_2_33_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2002. Types and Programming Languages ( 1 st ed.). The MIT Press . Benjamin C. Pierce. 2002. Types and Programming Languages (1st ed.). The MIT Press.","edition":"1"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"volume-title":"Lambda-definability and logical relations","author":"Plotkin Gordon","key":"e_1_2_2_35_1","unstructured":"Gordon Plotkin . 1973. Lambda-definability and logical relations . Edinburgh University . Gordon Plotkin. 1973. Lambda-definability and logical relations. Edinburgh University."},{"volume-title":"TACS \u201991","author":"Reynolds John C.","key":"e_1_2_2_36_1","unstructured":"John C. Reynolds . 1991. The Coherence of Languages with Intersection Types . In TACS \u201991 . Springer-Verlag , 675\u2013700. John C. Reynolds. 1991. The Coherence of Languages with Intersection Types. In TACS \u201991. Springer-Verlag, 675\u2013700."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000242"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80001-2"},{"key":"e_1_2_2_40_1","volume-title":"Intensional interpretations of functionals of finite type I. The journal of symbolic logic 32, 2","author":"Tait William W","year":"1967","unstructured":"William W Tait . 1967. Intensional interpretations of functionals of finite type I. The journal of symbolic logic 32, 2 ( 1967 ), 198\u2013212. William W Tait. 1967. Intensional interpretations of functionals of finite type I. The journal of symbolic logic 32, 2 (1967), 198\u2013212."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_2_2_42_1","volume-title":"ML\/OCaml","author":"White Leo","year":"2014","unstructured":"Leo White , Fr\u00e9d\u00e9ric Bour , and Jeremy Yallop . 2014. Modular implicits . In ML\/OCaml 2014 . Leo White, Fr\u00e9d\u00e9ric Bour, and Jeremy Yallop. 2014. Modular implicits. In ML\/OCaml 2014."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242752"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341695","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341695","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:30Z","timestamp":1750200090000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341695"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":40,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341695"],"URL":"https:\/\/doi.org\/10.1145\/3341695","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}