Cochis: Deterministic and coherent implicits

Implicit Progamming (IP) mechanisms infer values by a type-directed resolution process, 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 the desirability of coherence, ensuring each implicit has a unique resolution; 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 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 coherence and avoiding ambiguity. Cochis supports local scoping, overlapping instances, first-class instances, and higher-order rules, while remaining type safe and coherent. Cochis has a compact formulation. 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 and coherent. 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 focussing.nrpages: 51status: publishe