COCHIS: Stable and coherent implicits

Tom Schrijvers, Bruno C.D.S. Oliveira, Philip Wadler, Koar Marnitirosian

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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.
Original languageEnglish
Pages (from-to)1-82
Number of pages82
JournalJournal of Functional Programming
Volume29
Issue numbere3
Early online date8 Feb 2019
DOIs
Publication statusE-pub ahead of print - 8 Feb 2019

Fingerprint

Dive into the research topics of 'COCHIS: Stable and coherent implicits'. Together they form a unique fingerprint.

Cite this