File Download
There are no files associated with this item.
Links for fulltext
(May Require Subscription)
- Publisher Website: 10.1017/S0956796818000242
- Scopus: eid_2-s2.0-85061332629
- WOS: WOS:000458115000001
- Find via
Supplementary
- Citations:
- Appears in Collections:
Article: COCHIS: Stable and coherent implicits
Title | COCHIS: Stable and coherent implicits |
---|---|
Authors | |
Issue Date | 2019 |
Publisher | Cambridge 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? |
Abstract | Implicit 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 Identifier | http://hdl.handle.net/10722/301340 |
ISSN | 2023 Impact Factor: 1.1 2023 SCImago Journal Rankings: 0.484 |
ISI Accession Number ID |
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Schrijvers, T | - |
dc.contributor.author | Dos Santos Oliveira, BC | - |
dc.contributor.author | Wadler, P | - |
dc.contributor.author | Marntirosian, K | - |
dc.date.accessioned | 2021-07-27T08:09:39Z | - |
dc.date.available | 2021-07-27T08:09:39Z | - |
dc.date.issued | 2019 | - |
dc.identifier.citation | Journal of Functional Programming, 2019, v. 29, p. article no. e3 | - |
dc.identifier.issn | 0956-7968 | - |
dc.identifier.uri | http://hdl.handle.net/10722/301340 | - |
dc.description.abstract | Implicit 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.language | eng | - |
dc.publisher | Cambridge University Press. The Journal's web site is located at http://journals.cambridge.org/action/displayJournal?jid=JFP | - |
dc.relation.ispartof | Journal of Functional Programming | - |
dc.rights | Journal of Functional Programming. Copyright © Cambridge University Press. | - |
dc.rights | This 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.title | COCHIS: Stable and coherent implicits | - |
dc.type | Article | - |
dc.identifier.email | Dos Santos Oliveira, BC: bruno@cs.hku.hk | - |
dc.identifier.authority | Dos Santos Oliveira, BC=rp01786 | - |
dc.description.nature | link_to_subscribed_fulltext | - |
dc.description.nature | link_to_subscribed_fulltext | - |
dc.identifier.doi | 10.1017/S0956796818000242 | - |
dc.identifier.scopus | eid_2-s2.0-85061332629 | - |
dc.identifier.hkuros | 323727 | - |
dc.identifier.volume | 29 | - |
dc.identifier.spage | article no. e3 | - |
dc.identifier.epage | article no. e3 | - |
dc.identifier.isi | WOS:000458115000001 | - |
dc.publisher.place | United Kingdom | - |