{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T04:05:53Z","timestamp":1746072353851,"version":"3.40.4"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2013,4,9]],"date-time":"2013-04-09T00:00:00Z","timestamp":1365465600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/2.0"},{"start":{"date-parts":[[2013,4,9]],"date-time":"2013-04-09T00:00:00Z","timestamp":1365465600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/2.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Braz Comput Soc"],"published-print":{"date-parts":[[2013,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Algorithms for constraint set satisfiability and simplification of Haskell type class constraints are used during type inference in order to allow the inference of more accurate types and to detect ambiguity. Unfortunately, both constraint set satisfiability and simplification are in general undecidable, and the use of these algorithms may cause non-termination of type inference. This paper presents algorithms for these problems that terminate on any given input, based on the use of a criterion that is tested on each recursive step. The use of this criterion eliminates the need of imposing syntactic conditions on Haskell type class and instance declarations in order to guarantee termination of type inference in the presence of multi-parameter type classes, and allows program compilation without the need of compiler flags for lifting such restrictions. Undecidability of the problems implies the existence of instances for which the algorithm incorrectly reports unsatisfiability, but we are not aware of any practical example where this occurs.<\/jats:p>","DOI":"10.1007\/s13173-013-0107-9","type":"journal-article","created":{"date-parts":[[2013,4,8]],"date-time":"2013-04-08T09:25:05Z","timestamp":1365413105000},"page":"423-432","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Terminating constraint set satisfiability and simplification algorithms for context-dependent overloading"],"prefix":"10.1007","volume":"19","author":[{"given":"Rodrigo","family":"Ribeiro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlos","family":"Camar\u00e3o","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luc\u00edlia","family":"Figueiredo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,4,9]]},"reference":[{"key":"107_CR1","unstructured":"Gill A (2006) MTL\u2013The Monad Transformer Library. http:\/\/hackage.haskell.org\/package\/mtl"},{"key":"107_CR2","doi-asserted-by":"crossref","unstructured":"Baader F, Snyder W (2001) Unification theory. In: Robinson J., Voronkov A (eds) Handbook of Automated Reasoning, Elsevier Science Publishers, vol. 1, pp 447\u2013533","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"107_CR3","doi-asserted-by":"crossref","unstructured":"Camar\u00e3o C, Figueiredo L, Vasconcellos C (2004) Constraint-set Satisfiability for Overloading. In: Proc. of the 6th ACM SIGPLAN International Conf. on Principles and Practice of Declarative Programming (PPDP\u201904), pp 67\u201377","DOI":"10.1145\/1013963.1013974"},{"key":"107_CR4","unstructured":"Camar\u00e3o C, Ribeiro R, Figueiredo L, Vasconcellos C (2009) A Solution to Haskell\u2019s Multi-Parameter Type Class Dilemma. In: Proc. of the 13th Brazilian Symposium on Programming Languages (SBLP\u20192009), pp 5\u201318. http:\/\/www.dcc.ufmg.br\/camarao\/CT\/solution-to-mptc-dilemma.pdf"},{"issue":"2","key":"107_CR5","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/227699.227700","volume":"18","author":"C Hall","year":"1996","unstructured":"Hall C, Hammond K, Jones SP, Wadler P (1996) Type Classes in Haskell. ACM Trans Program Lang Syst 18(2):109\u2013138","journal-title":"ACM Trans Program Lang Syst"},{"key":"107_CR6","unstructured":"Smith G (1991) Polymorphic type inference for languages with overloading and subtyping. Ph.D. thesis, Cornell Univ."},{"key":"107_CR7","doi-asserted-by":"crossref","unstructured":"Jones M, Diatchki I (2008) Language and Program Design for Functional Dependencies. In: ACM SIGPLAN Haskell, Workshop, pp 87\u201398","DOI":"10.1145\/1543134.1411298"},{"key":"107_CR8","unstructured":"Jones SP et al. (2003) The Haskell 98 Language and Libraries: The Revised Report. J Func Prog 13(1):0\u2013255. http:\/\/www.haskell.org\/definition\/"},{"key":"107_CR9","unstructured":"Zhao L (2002) Solving and Creating Difficult Instances of Posts Correspondence Problem. Department of Computer Science, University of Alberta, Master\u2019s thesis"},{"key":"107_CR10","doi-asserted-by":"crossref","unstructured":"Chakravarty M, Keller G, Jones SP (2005) Associated type synonyms. In: Proc. of the 10th ACM SIGPLAN International Conf. on Functional Programming (ICFP\u201905), pp 241\u2013253","DOI":"10.1145\/1086365.1086397"},{"key":"107_CR11","doi-asserted-by":"crossref","unstructured":"Chakravarty M, Keller G, Jones SP, Marlow S (2005) Associated types withclass.In: Proc. of the ACM Symp. on Principles of Prog. Languages (POPL\u201905), pp 1\u201313","DOI":"10.1145\/1040305.1040306"},{"key":"107_CR12","doi-asserted-by":"crossref","unstructured":"Jones M (1994) Qualified Types. Cambridge University Press, Cambridge","DOI":"10.1017\/CBO9780511663086"},{"key":"107_CR13","doi-asserted-by":"crossref","unstructured":"Jones M (1995) Simplifying and Improving Qualified Types. In: Proc. of the ACM Conf. on Functional Prog. and Comp. Architecture (FPCA\u201995), pp 160\u2013169","DOI":"10.1145\/224164.224198"},{"key":"107_CR14","doi-asserted-by":"crossref","unstructured":"Jones M (2000) Type Classes with Functional Dependencies. In: Proc. of the European Symp. on Programming (ESOP\u20192000). LNCS 1782","DOI":"10.1007\/3-540-46425-5_15"},{"issue":"1","key":"107_CR15","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1017\/S0956796806006137","volume":"17","author":"M Sulzmann","year":"2007","unstructured":"Sulzmann M, Duck G, Jones SP, Stuckey P (2007) Understanding functional dependencies via constraint handling rules. J Funct Program 17(1):83\u2013129","journal-title":"J Funct Program"},{"key":"107_CR16","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R Milner","year":"1978","unstructured":"Milner R (1978) A theory of type polymorphism in programming. J Comput Syst Sci 17:348\u2013375","journal-title":"J Comput Syst Sci"},{"issue":"6","key":"107_CR17","doi-asserted-by":"publisher","first-page":"1216","DOI":"10.1145\/1108970.1108974","volume":"27","author":"P Stuckey","year":"2005","unstructured":"Stuckey P, Sulzmann M (2005) A Theory of Overloading. ACM Trans Prog Lang Syst (TOPLAS) 27(6):1216\u20131269","journal-title":"ACM Trans Prog Lang Syst (TOPLAS)"},{"key":"107_CR18","doi-asserted-by":"crossref","unstructured":"Wadler P, Blott S (1989) How to make ad-hoc polymorphism less ad-hoc. In: Proc. of the 16th ACM Symp. on Principles of Prog. Lang. (POPL\u201989), pp 60\u201376. ACM Press, New York","DOI":"10.1145\/75277.75283"},{"key":"107_CR19","unstructured":"Jones SP et al (1998) GHC\u2013The Glasgow Haskell Compiler. http:\/\/www.haskell.org\/ghc\/"},{"key":"107_CR20","unstructured":"Jones SP et al (2011) GHC\u2013The Glasgow Haskell Compiler 7.0.4 User\u2019s Manual. http:\/\/www.haskell.org\/ghc\/"}],"container-title":["Journal of the Brazilian Computer Society"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13173-013-0107-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s13173-013-0107-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s13173-013-0107-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13173-013-0107-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T03:32:15Z","timestamp":1745983935000},"score":1,"resource":{"primary":{"URL":"https:\/\/journal-bcs.springeropen.com\/articles\/10.1007\/s13173-013-0107-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4,9]]},"references-count":20,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["107"],"URL":"https:\/\/doi.org\/10.1007\/s13173-013-0107-9","relation":{},"ISSN":["0104-6500","1678-4804"],"issn-type":[{"type":"print","value":"0104-6500"},{"type":"electronic","value":"1678-4804"}],"subject":[],"published":{"date-parts":[[2013,4,9]]},"assertion":[{"value":"24 August 2012","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 March 2013","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 April 2013","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}