3

考虑以下程序，它仅在启用不连贯实例的情况下编译：

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE IncoherentInstances #-}

main = do
  print (g (undefined :: Int))
  print (g (undefined :: Bool))
  print (g (undefined :: Char))

data True

class CA t where
  type A t; type A t = True
  fa :: t -> String
instance CA Int where
  fa _ = "Int"

class CB t where
  type B t; type B t = True
  fb :: t -> String
instance CB Bool where
  fb _ = "Bool"

class CC t where
  type C t; type C t = True
  fc :: t -> String
instance CC Char where
  fc _ = "Char"

class CAll t t1 t2 t3 where
  g :: (t1 ~ A t, t2 ~ B t, t3 ~ C t) => t -> String

instance (CA t) => CAll t True  t2   t3  where g = fa
instance (CB t) => CAll t  t1  True  t3  where g = fb
instance (CC t) => CAll t  t1   t2  True where g = fc

当编译没有不连贯的实例时，它声称多个实例匹配。这似乎意味着当允许不连贯的实例时，将任意选择实例。

除非我非常幸运，否则这将导致编译错误，因为在大多数情况下不会满足实例约束。

但是对于不连贯的实例，我没有得到任何编译错误，并且确实得到了选择“正确”实例的以下输出：

"Int"
"Bool"
"Char"

所以我只能在这里总结几件事之一：

  1. GHC 正在回溯实例上下文故障（它说它在自己的文档中没有这样做）
  2. GHC 实际上知道只有一个匹配的实例，但没有足够的勇气使用它，除非打开不连贯的实例
  3. 我刚刚非常幸运（三分之一3 = 27 机会）
  4. 其他事情正在发生。

我怀疑答案是 4（可能与 2 结合）。我想要任何答案来解释这里发生了什么，以及在不连贯的实例中我可以在多大程度上依赖这种行为？如果它是可靠的，那么我似乎可以使用这种行为来制作相当复杂的类层次结构，实际上它的行为有点像子类型化，例如我可以说所有类型的 A 类和 B 类都在 C 类中，并且实例编写者可以为A 无需显式地为 C 创建一个实例。

编辑：

我怀疑答案与GHC 文档中的这个有关：

  1. 找到与目标约束匹配的所有实例 I；也就是说，目标约束是 I 的替换实例。这些实例声明是候选。
  2. 消除以下两项都成立的任何候选人 IX：
    • 还有另一个更具体的候选 IY；也就是说，IY 是 IX 的替代实例，反之则不然。
    • IX 是可重叠的，或者 IY 是重叠的。（这种“要么/或”设计，而不是“两者/和”设计，允许客户端故意覆盖库中的实例，而无需更改库。）

  3. 如果只剩下一个不连贯的候选者，则选择它。如果所有剩余的候选人都语无伦次，请选择一个任意的候选人。否则搜索失败（即当不止一个幸存的候选者不是不连贯的时候）。

  4. 如果所选候选者（来自上一步）不连贯，则搜索成功，并返回该候选者。

  5. 如果不是，则查找与目标约束一致但不匹配的所有实例。当目标约束被进一步实例化时，此类非候选实例可能匹配。如果全部不连贯，则搜索成功，返回选中的候选；如果不是，则搜索失败。

如果我错了，请纠正我，但无论是否选择了不连贯的实例，在第一步中，只有一个实例“匹配”。在不连贯的情况下，我们在第 4 步与那个“匹配”的情况发生冲突。但在不连贯的情况下，我们然后转到第 4 步，即使只有一个实例“匹配”，我们发现其他实例“统一” . 所以我们必须拒绝。

这种理解正确吗？

如果是这样，有人可以准确解释“匹配”和“统一”的含义，以及它们之间的区别吗？

4

0 回答 0