为啥这个 Haskell 代码使用fundeps 进行类型检查，但对类型族产生不可触碰的错误？

Posted 2023-02-19

【中文标题】为啥这个 Haskell 代码使用fundeps 进行类型检查，但对类型族产生不可触碰的错误？

【英文标题】：Why does this Haskell code typecheck with fundeps but produce an untouchable error with type families?为什么这个 Haskell 代码使用fundeps 进行类型检查，但对类型族产生不可触碰的错误？

【发布时间】：2018-05-23 21:46:55

【问题描述】：

给定一些类型定义：

data A
data B (f :: * -> *)
data X (k :: *)

……还有这个类型类：

class C k a | k -> a

...这些（出于最小示例的目的而高度人为的）函数定义类型检查：

f :: forall f. (forall k. (C k (B f)) => f k) -> A
f _ = undefined

g :: (forall k. (C k (B X)) => X k) -> A
g = f

但是，如果我们使用类型族而不是具有功能依赖的类：

type family F (k :: *)

...那么等价的函数定义无法进行类型检查：

f :: forall f. (forall k. (F k ~ B f) => f k) -> A
f _ = undefined

g :: (forall k. (F k ~ B X) => X k) -> A
g = f

• Couldn't match type ‘f0’ with ‘X’
    ‘f0’ is untouchable
      inside the constraints: F k ~ B f0
      bound by a type expected by the context:
                 F k ~ B f0 => f0 k
  Expected type: f0 k
    Actual type: X k
• In the expression: f
  In an equation for ‘g’: g = f

我阅读了 the OutsideIn(X) paper 的第 5.2 节，其中描述了可触摸和不可触摸的类型变量，我有点了解这里发生了什么。如果我向f 添加一个额外的参数，将f 的选择推到内部forall 之外，那么程序会进行类型检查：

f :: forall f a. f a -> (forall k. (F k ~ B f) => f k) -> A
f _ _ = undefined

g :: forall a. X a -> (forall k. (F k ~ B X) => X k) -> A
g = f

但是，在这个特定示例中，让我特别困惑的是为什么函数依赖具有不同的行为。我曾多次听到人们声称，像这样的函数依赖关系相当于一个类型族加上一个相等性，但这表明这实际上并非如此。

在这种情况下，函数依赖提供了哪些信息以允许以类型族没有的方式实例化 f？

【问题讨论】：

请注意，g = f @ X 也输入检查。推理算法似乎没有承诺将类型变量f 选择为X。我不明白为什么——通常是因为f 的另一个值使(forall k. (F k ~ B f) => f k) -> A 类型等于(forall k. (F k ~ B X) => X k) -> A。在这里，f ~ X 似乎是我唯一的解决方案（不是吗？）。很有趣。

@chi 我也这么认为，但我对类型检查器的这种特殊情况了解不多，无法自信地打开一个错误。也许无论如何我都应该开一张票，如果这是预期的行为，我至少可能会知道为什么？

确实很有趣！我现在已经两次循环了我的观点，即是否应该使用 既不 fundeps 而不是类型族，或者只使用fundeps，或两者兼而有之。我只是不太了解如何解决约束来决定。但至少我不认为只有fundep版本才能工作是不可信的：关键的区别似乎是类型类及其超类可以“解开”（f从B f中提取），但是从这是不可能的等式约束。

不是一个答案，但在你的观点上“我听说人们声称像这样的函数依赖关系相当于一个类型族加上一个平等” - 是的，这有点过于简单化了。当您考虑 Core 时，您可以看到语义差异来自何处。类型族实例表示为***强制，因此type instance F Int = Bool 变成f_int :: F Int ~ Bool。 Fundeps 只是在统一期间显示为约束，它们不会影响强制。这就是为什么它是hard to convert between them。

抱歉，我也没有答案，但请注意：您没有显示 FunDep 版本“允许实例化 f”。因为您还没有为C 声明任何实例（并让f 使用它们）。类型族验证比 FunDeps 更迫切。所以你可能会认为实际上这两种形式在某种意义上是等价的：Type family 形式不编译； FunDep 表单没有f 的实例化。也许这就是您只能定义f _ = undefined 的原因。所以为C声明一个实例；尝试将f 应用于某事。同样尝试申请g。

【参考方案1】：

我不知道我是否应该将其发布为答案，因为它仍然很容易挥手，但我确实认为这就是本质上发生的事情：

要评估(C k (B X)) => X k 值，您必须为k 选择具体类型，并指向满足约束条件的instance C k (B X)。为此，您必须说明类型类的a 参数具有B f 的形式，编译器可以从中提取f 类型（并在这种情况下找出它是X）——重要的是，它可以在实际查看实例之前执行此操作，这将是f 变得不可触摸的点。

要评估(F k ~ B X) => X k，它有点不同。这里你不需要指向一个具体的实例，你只需要保证如果编译器查找F k的类型族，那么这个类型将与B X的类型相同.但是在实际查找实例之前，编译器无法在此处推断F k 具有B f 的形式，因此也不能使用它来将f 与外部量化参数统一，因为不可触及。

因此，GHC 的行为至少不是完全不合理的。我仍然不确定它是否应该这样做。

【讨论】：

虽然你说的有些道理，但我对这个答案有点怀疑。原因如下：如果将data B 更改为type family B，具有功能依赖的版本仍然会进行类型检查！这似乎与您对 fundep 版本为何以这种方式工作的解释相矛盾，因为如果 B 是一个类型族，B f ~ B X 并不意味着 f ~ X。

【参考方案2】：

好的，我有机会玩这个。有几个分心：

在 Type Family 版本中，仅 f 的定义会给出错误 'f0' is untouchable。 （您可以使用AllowAmbiguousTypes 来抑制它；这只是推迟了针对g 出现的错误。）让我们忽略g。

如果没有AllowAmbiguousTypes，则 f 的错误消息会提供更多信息：

• Couldn't match type ‘f0’ with ‘f’
    ‘f0’ is untouchable
      inside the constraints: F k ~ B f0
      bound by the type signature for:
                 f :: F k ~ B f0 => f0 k
  ‘f’ is a rigid type variable bound by
    the type signature for:
      f :: forall (f :: * -> *). (forall k. F k ~ B f => f k) -> A
  Expected type: f0 k
    Actual type: f k

啊哈！ rigid type variable 问题。我猜是因为f 是由来自k 的等式约束固定的，这也是刚性的，因为...

转到没有g 的FunDep 版本，我们可以在哪些类型中调用f？试试

f (undefined undefined :: X a)           -- OK
f (undefined "string"  :: X String)      -- rejected
f  Nothing                               -- OK
f (Just 'c')                             -- rejected

拒绝消息（对于X String 示例）是

• Couldn't match type ‘k’ with ‘String’
  ‘k’ is a rigid type variable bound by
    a type expected by the context:
      forall k. C k (B X) => X k
  Expected type: X k
    Actual type: X String
• In the first argument of ‘f’, namely
    ‘(undefined "string" :: X String)’

注意消息是关于 k，不是 f，这是由 FunDep 确定的——或者如果我们能找到合适的 k。

说明

函数f 的签名表示k 是存在量化/更高等级的。然后我们不能允许任何关于k 的类型信息逃逸到周围的上下文中。我们不能为k 提供任何（非底部）值，因为它的类型会侵入forall。

这是一个更简单的例子：

f2 :: forall f. (forall k. f k) -> A
f2 _ = undefined

f2 Nothing                                 -- OK
f2 (Just 'c')                              -- rejected rigid type var

所以原来的FunDep 版本编译是一种干扰：它不能被居住。 （根据我之前的怀疑，这是FunDeps 的常见症状。）

【讨论】：

顺便说一句，您会收到与此签名 f :: forall f. (forall k. f ~ X => f k) -> A 类似的 f0 is untouchable 拒绝。看不到 Type Family 或 FunDep。