File Download

There are no files associated with this item.

  Links for fulltext
     (May Require Subscription)
Supplementary

Article: COCHIS: Stable and coherent implicits

TitleCOCHIS: Stable and coherent implicits
Authors
Issue Date2019
PublisherCambridge University Press. The Journal's web site is located at http://journals.cambridge.org/action/displayJournal?jid=JFP
Citation
Journal of Functional Programming, 2019, v. 29, p. article no. e3 How to Cite?
AbstractImplicit programming (IP) mechanisms infer values by type-directed resolution, making programs more compact and easier to read. Examples of IP mechanisms include Haskell’s type classes, Scala’s implicits, Agda’s instance arguments, Coq’s type classes and Rust’s traits. The design of IP mechanisms has led to heated debate: proponents of one school argue for the desirability of strong reasoning properties, while proponents of another school argue for the power and flexibility of local scoping or overlapping instances. The current state of affairs seems to indicate that the two goals are at odds with one another and cannot easily be reconciled. This paper presents COCHIS, the Calculus Of CoHerent ImplicitS, an improved variant of the implicit calculus that offers flexibility while preserving two key properties: coherence and stability of type substitutions. COCHIS supports polymorphism, local scoping, overlapping instances, first-class instances and higher-order rules, while remaining type-safe, coherent and stable under type substitution. We introduce a logical formulation of how to resolve implicits, which is simple but ambiguous and incoherent, and a second formulation, which is less simple but unambiguous, coherent and stable. Every resolution of the second formulation is also a resolution of the first, but not conversely. Parts of the second formulation bear a close resemblance to a standard technique for proof search called focusing. Moreover, key for its coherence is a rigorous enforcement of determinism.
Persistent Identifierhttp://hdl.handle.net/10722/301340
ISSN
2020 Impact Factor: 0.529
2020 SCImago Journal Rankings: 0.350

 

DC FieldValueLanguage
dc.contributor.authorSchrijvers, T-
dc.contributor.authorDos Santos Oliveira, BC-
dc.contributor.authorWadler, P-
dc.contributor.authorMarntirosian, K-
dc.date.accessioned2021-07-27T08:09:39Z-
dc.date.available2021-07-27T08:09:39Z-
dc.date.issued2019-
dc.identifier.citationJournal of Functional Programming, 2019, v. 29, p. article no. e3-
dc.identifier.issn0956-7968-
dc.identifier.urihttp://hdl.handle.net/10722/301340-
dc.description.abstractImplicit programming (IP) mechanisms infer values by type-directed resolution, making programs more compact and easier to read. Examples of IP mechanisms include Haskell’s type classes, Scala’s implicits, Agda’s instance arguments, Coq’s type classes and Rust’s traits. The design of IP mechanisms has led to heated debate: proponents of one school argue for the desirability of strong reasoning properties, while proponents of another school argue for the power and flexibility of local scoping or overlapping instances. The current state of affairs seems to indicate that the two goals are at odds with one another and cannot easily be reconciled. This paper presents COCHIS, the Calculus Of CoHerent ImplicitS, an improved variant of the implicit calculus that offers flexibility while preserving two key properties: coherence and stability of type substitutions. COCHIS supports polymorphism, local scoping, overlapping instances, first-class instances and higher-order rules, while remaining type-safe, coherent and stable under type substitution. We introduce a logical formulation of how to resolve implicits, which is simple but ambiguous and incoherent, and a second formulation, which is less simple but unambiguous, coherent and stable. Every resolution of the second formulation is also a resolution of the first, but not conversely. Parts of the second formulation bear a close resemblance to a standard technique for proof search called focusing. Moreover, key for its coherence is a rigorous enforcement of determinism.-
dc.languageeng-
dc.publisherCambridge University Press. The Journal's web site is located at http://journals.cambridge.org/action/displayJournal?jid=JFP-
dc.relation.ispartofJournal of Functional Programming-
dc.rightsJournal of Functional Programming. Copyright © Cambridge University Press.-
dc.rightsThis article has been published in a revised form in [Journal] [http://doi.org/XXX]. This version is free to view and download for private research and study only. Not for re-distribution, re-sale or use in derivative works. © copyright holder.-
dc.titleCOCHIS: Stable and coherent implicits-
dc.typeArticle-
dc.identifier.emailDos Santos Oliveira, BC: bruno@cs.hku.hk-
dc.identifier.authorityDos Santos Oliveira, BC=rp01786-
dc.description.naturelink_to_subscribed_fulltext-
dc.description.naturelink_to_subscribed_fulltext-
dc.identifier.doi10.1017/S0956796818000242-
dc.identifier.scopuseid_2-s2.0-85061332629-
dc.identifier.hkuros323727-
dc.identifier.volume29-
dc.identifier.spagearticle no. e3-
dc.identifier.epagearticle no. e3-
dc.publisher.placeUnited Kingdom-

Export via OAI-PMH Interface in XML Formats


OR


Export to Other Non-XML Formats