一句话：提出 COCHIS 演算，在保持类型安全、连贯性与类型替换稳定性的同时支持多态、局部作用域、重叠实例与高阶规则。
隐式编程（IP）机制通过类型导向的解析来推断值，使程序更紧凑易读，Haskell 类型类、Scala implicits、Agda 实例参数等均属此类。其设计长期存在争论：一方强调强推理性质，另一方强调局部作用域与重叠实例带来的灵活性与表达力，二者似乎难以兼得。本文提出 COCHIS（Calculus Of CoHerent ImplicitS），是隐式演算的改进变体，在保持连贯性（coherence）与类型替换稳定性这两个关键性质的同时，支持多态、局部作用域、重叠实例、一等实例与高阶规则，并保持类型安全。作者给出隐式解析的两种逻辑表述：第一种简单但存在歧义且不连贯；第二种虽不简单，却无歧义、连贯且在类型替换下稳定。第二种表述的每个解析都是第一种的解析，反之不成立。第二种表述的部分内容与证明搜索中的 focusing 技术高度相似，而实现连贯性的关键在于严格强制确定性。
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.
@article{paperbot721,
title = {COCHIS: Stable and coherent implicits},
author = {TOM SCHRIJVERS and BRUNO C.D.S. OLIVEIRA and PHILIP WADLER and KOAR MARNTIROSIAN},
journal = {Journal of Functional Programming},
volume = {29},
year = {2019},
doi = {10.1017/s0956796818000242}
}