Scala是否保证存在隐含的连贯性？

Question

文章Type classes: confluence, coherence and global uniqueness提出以下几点 -

[Coherence]指出程序的每个不同的有效类型派生导致具有相同动态语义的结果程序。

[..]

那么，人们在将Scala类型类与Haskell类型类进行比较时经常会引用什么呢？我将把它称为实例的全局唯一性，定义为：在完全编译的程序中，对于任何类型，给定类型类最多只有一个实例解析。具有本地类型类实例（如Scala）的语言通常没有此属性，但在Haskell中，我们发现在构建集合等抽象时，此属性非常方便。

如果你看看Modular implicits上的这篇论文，它说 -

[...] Scala的连贯性可以依赖于非模糊性而不是规范性的较弱属性。这意味着您可以在程序中定义多个类型为Showable [Int]的隐式对象，而不会导致错误。相反，如果隐式参数的分辨率不明确，Scala会发出错误。例如，如果在将show应用于Int时，两个Showable [Int]类型的隐式对象在范围内，则编译器将报告歧义错误。

这两者都给人的印象是Scala确实确保了一致性，但并不能确保实例的全局唯一性。

但是，如果你看看Martin Odersky的评论（1，2），似乎术语连贯性被用作“实例的唯一性”的简写，这可以解释术语“局部连贯性”和“全局连贯性”。

1. 这只是一个不幸的例子，同一个术语被用来表示两种不同的东西吗？它们肯定是截然不同的 - OCaml的模块化含义确保了一致性（根据第一个定义），但不保证实例的全局唯一性。
2. Scala是否在隐含存在的情况下保证一致性（根据第一个定义）？

Answer 1

我认为在这种情况下他们的意思相同。只有在获得实例/隐式值的方法不止一种时，才会对连贯性产生疑问; “每个不同的有效类型派生”只有在不止一次打字派生时才有意义。 Scala和Haskell都不允许在编译时实例，这可能会导致模糊的派生。

Scala

Odersky的评论说它适用于Scala：只有一种本地解析实例的方法。换句话说，只有一个有效的本地类型派生。很简单，它与自身一致。我不清楚在Scala中讨论全局一致性甚至是有意义的，但如果确实如此，Scala肯定没有它：

object Object1 {
  implicit val i: Int  = 9
  println(implicitly[Int])    // valid typing derivation of `Int` => printing 9
}
object Object2 {
  implicit val i: Int  = 10
  println(implicitly[Int])    // valid typing derivation of `Int` => printing 10
}

Haskell

由于Haskell实例是全局的，因此区分本地/全局一致性没有意义。

Haskell在编译时不允许有两个实例头与另一个实例头重叠的实例。这将查找类型派生转变为明确的非回溯搜索问题。非模糊性再次使我们保持连贯性。

有趣的是，GHC允许您使用-XIncoherentInstances放宽此要求，允许您编写本地非融合实例，也可能破坏全局一致性。