重叠实例 - 如何规避它们

Question

我是 Haskell 的初学者，所以请放纵一下。由于这里不重要的原因，我试图定义一个运算符<^>，它接受一个函数和一个参数，并通过参数返回函数的值，无论哪个函数和参数先出现。简而言之，我希望能够写出以下内容：

foo :: Int -> Int
foo x = x * x

arg :: Int
arg = 2

foo <^> arg -- valid, returns 4
arg <^> foo -- valid, returns 4

我试图通过类型族来实现这一点，如下所示：

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

class Combine t1 t2 where
    type Output t1 t2 :: *
    (<^>) :: t1 -> t2 -> Output t1 t2

instance Combine (a->b) a where
    type Output (a->b) a = b
    f <^> x = f x

instance Combine a (a->b) where
    type Output a a->b = b
    x <^> f = f x

在此代码中，GHC 抛出 Conflicting family instance declarations。我的猜测是，当 a->b 类型和 a 类型相同时，GHC 抱怨的重叠就会发生。我不太了解 Haskell，但我怀疑使用递归类型定义，可能能够构建这种情况。我有几个问题：

• 由于这是一个相当遥远的场景，在我的应用程序中永远不会发生（尤其是上面的 foo 和 arg 不会出现），我想知道是否有办法指定一个虚拟默认实例以在重叠的情况下使用？我尝试了不同的 OVERLAPS 和 OVERLAPPING 标志，但它们没有任何效果。
• 如果没有，有没有更好的方法来实现我想要的？

谢谢！

Answer 1

@chi 关闭；使用 FunDeps 或封闭类型家族的方法是可能的。但是 Combine 实例可能与 CTF Output 方程一样具有歧义/统一性。

当 chi 说 FunDep 代码被接受时，这只是对了一半：GHC plain 会引导您沿着花园小路走下去。它会接受这些实例，但是你发现你不能使用它们/你会收到奇怪的错误消息。请参阅“潜在重叠”中的用户指南。

如果您要解决可能不明确的Combine 约束，您可能会收到错误提示，建议您尝试IncoherentInstances（或INCOHERENT pragma）。不要那样做。你有一个真正不连贯的问题；所要做的就是将问题推迟到其他地方。总是可以避免 Incoherent - 只要您可以重新调整您的实例（如下所示）并且它们没有被锁定在库中。

请注意，由于潜在的歧义，另一个 Haskell 编译器 (Hugs) 不允许您这样写 Combine。它更正确地实现了 Haskell 的（未充分说明的）规则。

答案是使用一种重叠，其中一个实例更具体。您必须首先决定您希望采用哪种方式，以防出现歧义。我将选择以参数为前缀的函数：

{-# LANGUAGE UndecidableInstances, TypeFamilies #-}

instance {-# OVERLAPPING #-} (r ~ b)
         => Combine (a->b) a r  where ...

instance {-# OVERLAPPABLE #-} (Combine2 t1 t2 r)
         => Combine t1 t2 r  where
  (<^>) = revApp

class Combine2 t1 t2 r  | t1 t2 -> r  where
  revApp :: t1 -> t2 -> r

instance (b ~ r) => Combine2 a (a->b) r  where
  revApp x f = f x

请注意，Combine 的 OVERLAPPABLE 实例具有裸 tyvars，它是一个包罗万象的，所以它总是可以匹配的。编译器所要做的就是确定某个想要的约束是否是OVERLAPPING 实例的形式。

OVERLAPPABLE 实例上的Combine2 约束不小于头部，因此您需要UndecidableInstances。另请注意，推迟到Combine2 意味着如果编译器仍然无法解析，您可能会收到令人费解的错误消息。

谈到裸 tyvars/“始终匹配”，我使用了一个额外的技巧来使编译器非常努力地改进类型：实例头部有裸 r，具有 Equality 类型改进约束(b ~ r) =>。要使用~，您需要打开TypeFamilies，即使您没有编写任何类型族。

CTF 方法与此类似。您需要在 Output 上调用辅助类型函数的包罗万象的方程。你再次需要UndecidableInstances。

Answer 2

在我看来，这是个坏主意，但我会继续努力的。

一个可能的解决方案是切换到函数依赖。通常我倾向于避免使用类型族来支持类型族，但在这里它们使实例以简单的方式编译。

class Combine t1 t2 r | t1 t2 -> r where
    (<^>) :: t1 -> t2 -> r

instance Combine (a->b) a b where
    f <^> x = f x

instance Combine a (a->b) b where
    x <^> f = f x

请注意，如果我们使用多态函数，这个类可能会在类型推断期间引起问题。这是因为，使用多态函数，代码很容易变得模棱两可。

例如id <^> id 可以选择两个实例中的任何一个。上面，melpomene 已经报告了const <^> id 也是模棱两可的。

---

以下是弱相关，但还是想分享一下：

那么类型族呢？我尝试了一下，我发现了一个我不知道的限制。考虑封闭类型族

type family Output a b where
   Output (a->b) a = b
   Output a (a->b) = b

上面的代码可以编译，但是Output a (a->b) 类型被卡住了。第二个等式没有得到应用，好像第一个可能匹配。

通常在其他一些场景下我可以理解，但这里统一

Output (a' -> b') b' ~ Output a (a -> b)

似乎失败了，因为我们需要a ~ (a' -> b') ~ (a' -> a -> b)，这是不可能的，有限类型。出于某种原因，GHC 不使用此参数（它是否假装在此检查中存在无限类型？为什么？）

无论如何，这似乎使得用类型族替换fundeps 变得更加困难。我不知道为什么 GHC 接受我发布的基金代码，但拒绝 OP 的代码，除了使用类型族之外，它本质上是一样的。