{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T02:22:07Z","timestamp":1648866127965},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2013,3,15]],"date-time":"2013-03-15T00:00:00Z","timestamp":1363305600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/2.0"},{"start":{"date-parts":[[2013,3,15]],"date-time":"2013-03-15T00:00:00Z","timestamp":1363305600000},"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,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper discusses ambiguity in the context of languages that support context-dependent overloading, such as Haskell. A type system for a Haskell-like programming language that supports context-dependent overloading and follow the Hindley-Milner approach of providing context-free type instantiation, allows distinct derivations of the same type for ambiguous expressions. Such expressions are usually rejected by the type inference algorithm, which is thus not complete with respect to the type system. Also, Haskell\u2019s open world approach considers a definition of ambiguity that does not conform to the existence of two or more distinct type system derivations for the same type. The article presents an alternative approach, where the standard definition of ambiguity is followed. A type system is presented that allows only context-dependent type instantiation, enabling only one type to be derivable for each expression in a given typing context: the type of an expression can be instantiated only if required by the program context where the expression occurs. We define a notion of greatest instance type for each occurrence of an expression, which is used in the definition of a standard dictionary-passing semantics for core Haskell based on type system derivations, for which coherence is trivial. Type soundness is obtained as a result of disallowing all ambiguous expressions and all expressions involving unsatisfiability in the use of overloaded names. Following the standard definition of ambiguity, satisfiability is tested\u2014i.e.,\u00a0\u201cthe world is closed\u201d \u2014if only if overloading is (or should have been) resolved, that is, if and only if there exist unreachable variables in the constraints on types of expressions. Nowadays, satisfiability is tested in Haskell, in the presence of multi-parameter type classes, only upon the presence of functional dependencies or an alternative mechanism that specifies conditions for closing the world, and that may happen when there exist or not unreachable type variables in constraints. The satisfiability trigger condition is then given automatically, by the existence of unreachable variables in constraints, and does not need to be specified by programmers, using an extra mechanism.<\/jats:p>","DOI":"10.1007\/s13173-013-0103-0","type":"journal-article","created":{"date-parts":[[2013,3,14]],"date-time":"2013-03-14T14:31:42Z","timestamp":1363271502000},"page":"313-324","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Ambiguity and 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"}]}],"member":"297","published-online":{"date-parts":[[2013,3,15]]},"reference":[{"key":"103_CR1","unstructured":"Mitchell J (1996) Foundations of Programming Languages. MIT Press, Cambridge"},{"key":"103_CR2","unstructured":"Pierce B (2002) Types and Programming Languages. MIT Press, Cambridge"},{"key":"103_CR3","doi-asserted-by":"crossref","unstructured":"Jones M (1994) Qualified Types: Theory and Practice. Ph.D. thesis, Distinguished Dissertations in Computer Science. Cambridge Univ. Press, Cambridge","DOI":"10.1017\/CBO9780511663086"},{"issue":"6","key":"103_CR4","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)"},{"issue":"4\u20135","key":"103_CR5","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1017\/S0956796811000098","volume":"21","author":"D Vytiniotis","year":"2011","unstructured":"Vytiniotis D, Jones S, Schrijvers T, Sulzmann M (2011) OutsideIn(X): modular type inference with local assumptions. J Funct Program 21(4\u20135):333\u2013412","journal-title":"J Funct Program"},{"key":"103_CR6","doi-asserted-by":"crossref","unstructured":"Fax\u00e9n K (2003) Haskell and Principal Types. In: Proceedings 2003 ACM SIGPLAN Haskell, Workshop, pp 88\u201397","DOI":"10.1145\/871895.871905"},{"key":"103_CR7","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1017\/S0956796802004380","volume":"12","author":"K Fax\u00e9n","year":"2002","unstructured":"Fax\u00e9n K (2002) A static semantics for Haskell. J Funct Program 12:295\u2013357","journal-title":"J Funct Program"},{"key":"103_CR8","doi-asserted-by":"crossref","unstructured":"Camar\u00e3o C, Figueiredo L (1999) Type Inference for Overloading without Restrictions, Declarations or Annotations. In: Proceeding 4$${\\rm th}$$ Fuji International Symp. on Functional and Logic Programming (FLOPS\u201999), LNCS 1722, Springer-Verlag, New York, pp 37\u201352","DOI":"10.1007\/10705424_3"},{"key":"103_CR9","unstructured":"Jones SP, et al (2012) GHC\u2014the Glasgow Haskell compiler. http:\/\/www.haskell.org\/ghc\/"},{"issue":"2","key":"103_CR10","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 S, Wadler P (1996) Type classes in Haskell. ACM Trans Program Lang Syst 18(2):109\u2013138","journal-title":"ACM Trans Program Lang Syst"},{"key":"103_CR11","doi-asserted-by":"crossref","unstructured":"Chakravarty MG, Keller SP, Jones S (2005) Marlow: associated types with class. In: Proceeding ACM Symp. on Principles of Programming Languages (POPL\u201905), ACM Press, Florida, pp 1\u201313","DOI":"10.1145\/1040305.1040306"},{"key":"103_CR12","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/321250.321253","volume":"12","author":"J Robinson","year":"1965","unstructured":"Robinson J (1965) A machine-oriented logic based on the resolution principle. J ACM 12:32\u201341","journal-title":"J ACM"},{"key":"103_CR13","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/S0747-7171(85)80027-4","volume":"1","author":"E Eder","year":"1985","unstructured":"Eder E (1985) Properties of substitutions and unification. J Sym Comput 1:31\u201346","journal-title":"J Sym Comput"},{"key":"103_CR14","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/BFb0032046","volume":"443","author":"C Palamidessi","year":"1990","unstructured":"Palamidessi C (1990) Algebraic properties of idempotent substitutions. Lect Notes Comput Sci 443:386\u2013399","journal-title":"Lect Notes Comput Sci"},{"key":"103_CR15","unstructured":"Camar\u00e3o C, Ribeiro R, Figueiredo L, Vasconcellos C (2009) A Solution to Haskell\u2019s Multi-Parameter Type Class Dilemma. In: Proceeding $$13{\\rm th}$$ Brazilian Symp. on Programming Languages (SBLP\u20192009), pp 5\u201318. http:\/\/www.dcc.ufmg.br\/camarao\/CT\/solution-to-mptc-dilemma.pdf"},{"key":"103_CR16","doi-asserted-by":"crossref","unstructured":"Chakravarty M, Keller G, Jones S (2005) Associated type synonyms. In: Proceeding 10$${\\rm th}$$ ACM SIGPLAN International Conference on Functional Programming, pp 241\u2013253","DOI":"10.1145\/1090189.1086397"},{"key":"103_CR17","doi-asserted-by":"crossref","unstructured":"Jones M (1995) Simplifying and improving qualified types. In: Proceeding ACM Conf. on Functional Programming and Computer Architecture (FPCA\u201995), Cambridge University Press, Cambridge, pp 160\u2013169","DOI":"10.1145\/224164.224198"},{"key":"103_CR18","unstructured":"Smith G (1991) Polymorphic type inference for languages with overloading and subtyping. Ph.D. thesis, Cornell University, NY"},{"key":"103_CR19","unstructured":"Jones SP, others (2011) GHC\u2014The Glasgow Haskell Compiler 7.0.4 User\u2019s Manual. http:\/\/www.haskell.org\/ghc\/"},{"key":"103_CR20","doi-asserted-by":"crossref","unstructured":"Wadler P, Blott S (1989) How to make ad-hoc polymorphism less ad hoc. In: Proceeding 16$${\\rm th}$$ ACM Symp. on Principles of Programming Language (POPL\u201989), ACM Press, Florida, pp 60\u201376","DOI":"10.1145\/75277.75283"},{"key":"103_CR21","doi-asserted-by":"crossref","unstructured":"Peterson J, Jones M (1993) Implementing type classes. In: Proceeding ACM Conference on Programming Language Design and Implementation, SIGPLAN Notices 28(6), Florida, pp 227\u2013236","DOI":"10.1145\/173262.155112"},{"key":"103_CR22","unstructured":"Jones M (1994) Dictionary-free Overloading by Partial Evaluation. In: ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation"}],"container-title":["Journal of the Brazilian Computer Society"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13173-013-0103-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s13173-013-0103-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s13173-013-0103-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13173-013-0103-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T22:31:24Z","timestamp":1630535484000},"score":1,"resource":{"primary":{"URL":"https:\/\/journal-bcs.springeropen.com\/articles\/10.1007\/s13173-013-0103-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3,15]]},"references-count":22,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,9]]}},"alternative-id":["103"],"URL":"https:\/\/doi.org\/10.1007\/s13173-013-0103-0","relation":{},"ISSN":["0104-6500","1678-4804"],"issn-type":[{"value":"0104-6500","type":"print"},{"value":"1678-4804","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3,15]]},"assertion":[{"value":"1 October 2012","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 February 2013","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 March 2013","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}