为什么这个嵌套的类型类派生工作？

2024-05-20 • 问答

是的，这是一个不寻常的“为什么这样做”的问题。我有这段代码：

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}

data F a = A (F a) | B (a (F a)) -- a :: * -> *
deriving instance (forall b. Eq b => Eq (a b)) => Eq (F a)

-- the following errors,asking me to add (Eq b) into the context
deriving instance (forall b. Eq (a b)) => Eq (F a)

如果定义第二个版本会出错

data T a = C | D a deriving Eq
x = B C == B C

从逻辑的角度来看，将(Eq b)添加到约束应该类似于(forall b. Eq b && Eq (a b)) => Eq (F a)，因为我们需要将其保留在forall的范围内。可以想象，(Eq b) 是隐式假定的，就像大多数派生实例一样。但如果是这样，为什么第二个版本不起作用？

第一个推导等于下面的实例

instance (forall b. Eq b => Eq (f b)) => Eq (F f) where
  (==) :: F f -> F f -> Bool
  A a1 == A b1 = (==) @(F f)     a1 b1
  B a1 == B b1 = (==) @(f (F f)) a1 b1
  _    == _    = False

鉴于在 f (forall b. Eq b => Eq (f b)) 下等式是封闭的，(==) @(F f) 和 (==) @(f (F f))

需要以下约束

Eq (F f)
Eq (f (F f))

对于第一个是我们正在编写/派生的相等实例：Eq (F f) 在当前上下文中保持（Eq 在 f 下关闭）。因此该约束得到满足。

第二个要求我们提升的类型的相等性：Eq (f (F f)) 来自上下文：Eq 在 f 下被关闭。

如果我们使用 F f 实例化 b 我们会看到我们提升的类型支持相等 Eq (F f) => Eq (f (F f)) 如果我们定义的类型支持相等... 1.).

第二个实例在 GHC Head 上编译。

deriving instance (forall b. Eq (f b)) => Eq (F f)

如果您知道 Eq (f b) 对任何 b 成立，您可以通过实例化 来解决 1. 和 2. >b 和 F f。

在玩了一会儿之后，我想我已经解决了这个问题。很抱歉经常编辑问题！我把代码简单化了，没有仔细测试。

Database Inspector 派生一个需要 data T a = C | D a 的 Eq 实例。没有它，就不能满足 Eq a 前提。使用 forall b. Eq (T b)，我们可以使用 forall b. (Eq b) => Eq (T b) 获得 Eq b 上所需的相等谓词。

为什么这个嵌套的类型类派生工作？

zlzed888 回答：为什么这个嵌套的类型类派生工作？

大家都在问