Resolution and subtyping are two common mechanisms in programming languages. Resolution is used by features such as type classes or Scala-style implicits to synthesize values automatically from contextual type information. Subtyping is commonly used to automatically convert the type of a value into another compatible type. So far the two mechanisms have been considered independently of each other. This paper shows that, with a small extension, subtyping with intersection types can subsume resolution. This has three main consequences. Firstly, resolution does not need to be implemented as a separate mechanism. Secondly, the interaction between resolution and subtyping becomes apparent. Finally, the integration of resolution into subtyping enables first-class (implicit) environments. The extension that recovers the power of resolution via subtyping is the modus ponens rule of propositional logic. While it is easily added to declarative subtyping, significant care needs to be taken to retain desirable properties, such as transitivity and decidability of algorithmic subtyping, and coherence. To materialize these ideas we develop $\lambda_i^{\mathsf{MP}}$, a calculus that extends a iprevious calculus with disjoint intersection types, and develop its metatheory in the Coq theorem prover.

翻译：分辨率和亚型是编程语言中的两种常见机制。 分辨率被类型类或 Scala 式隐含的隐含功能用来自动合成背景型信息中的值。 亚型通常用来自动将一个值的类型转换成另一个兼容型。 到目前为止, 这两种机制已经相互独立地考虑过。 本文显示, 通过小扩展, 与交叉类型相交的亚型可以包含分辨率。 这有三个主要后果。 首先, 分辨率不需要作为一个单独的机制来实施。 其次, 分辨率和亚型之间的相互作用变得显而易见。 最后, 将分辨率整合到亚型中可以促成第一类( 隐含) 环境。 通过亚型转换恢复解析力的扩展是方略逻辑的扩展。 虽然它很容易被添加到声明性亚型中, 但需要小心保留可取的属性, 如算法子型的过渡性和变异性, 以及一致性。 要实现这些想法, 我们开发了 $\lamda_ i ⁇ maths {MP$。 $, a calculusulus 恢复了分辨率的交叉、 和交叉性。