在 GADT 中绑定时，函数依赖不统一

Question

在下面的代码中：

\n

class FD a b | a -> b\n\ndata Foo a where\n  Foo :: FD a b => b -> Foo a\n\nunFoo :: FD a b => Foo a -> b\nunFoo (Foo x) = x\n

\n

根据常识，这应该可行，因为aGADT 和函数中的约束是相同的，并且它确定b，但是这不会编译并出现以下错误：

\n

    \xe2\x80\xa2 Couldn't match expected type \xe2\x80\x98b\xe2\x80\x99 with actual type \xe2\x80\x98b1\xe2\x80\x99\n      \xe2\x80\x98b1\xe2\x80\x99 is a rigid type variable bound by\n        a pattern with constructor:\n          Foo :: forall a b. FD a b => b -> Foo a,\n        in an equation for \xe2\x80\x98unFoo\xe2\x80\x99\n        at src/Lib.hs:13:8-12\n      \xe2\x80\x98b\xe2\x80\x99 is a rigid type variable bound by\n        the type signature for:\n          unFoo :: forall a b. FD a b => Foo a -> b\n        at src/Lib.hs:12:1-29\n    \xe2\x80\xa2 In the expression: x\n      In an equation for \xe2\x80\x98unFoo\xe2\x80\x99: unFoo (Foo x) = x\n    \xe2\x80\xa2 Relevant bindings include\n        x :: b1 (bound at src/Lib.hs:13:12)\n        unFoo :: Foo a -> b (bound at src/Lib.hs:13:1)\n   |\n13 | unFoo (Foo x) = x\n   |                 ^\n

\n

它不起作用有什么充分的理由吗？

\n

Answer 1

@chi Fundeps 和 GADT 之间的相互作用……目前看起来相当糟糕。

我认为这比这更重要（不仅仅是“目前”，也不仅仅是 FunDeps）。

x无论编译器推断出in的类型

unFoo (Foo x) = ...

仅在 RHS 上有效，在 的比赛中(Foo x)。尝试裸露返回x会让任何假设消失。

比较一个更古老的等价物：在我们有了 GADT 之前，就有存在量化的数据构造器，所以

data Foo' a = forall b. FD a b => Foo' b

unFoo' :: FD a b => Foo' a -> b
unFoo' (Foo' x) = x

由于同样的原因无法编译。

或者尝试编写一个实例也会FD遇到同样的rigid type variable麻烦：

class FD a b | a -> b  where
  unFoom :: Foo a -> b
instance FD Int Bool  where
  unFoom (Foo x) = x    -- Couldn't match expected type `Bool' with actual type `b'

您可能会发现 Hugs 的错误消息更具启发性（对于存在数据类型）

*** Because        : cannot instantiate Skolem constant

我不相信这与 FunDeps 有很大关系。比较

data FooN a where           
  FooN :: Num b => b -> FooN a

unFooN :: Num b => FooN a -> b
-- unFooN (FooN x) = x + 1                 -- rejected
unFooN (FooN x) = const undefined (x + 1)  -- accepted (but useless)

z = 1 + unFooN (FooN 7)                    -- accepted (for useless unFooN)

出于同样的原因被拒绝：该假设x :: Num b => b仅在比赛内有效。

补充：（回应评论）

扩展“仅在 RHS 上有效，在(Foo x)”上的比赛中：

• 一般来说，GADT 有许多构造函数，每个构造函数可能都有不同的约束。
• （或者实际上我们可能有一个没有构造函数的值，如 中所示(undefined :: Foo t)。）
• 因此，匹配必须在应用“仅在 RHS 上有效”之前查看构造函数。

出于这些目的，FunDep 被视为任何其他约束，因此 OP 的问题就像这种FooN情况。（存在主义b仍然仅限于 RHS。）

@dfeuer使用类型族的重新设计不依赖于 tyvar 的范围b；类型族适用于a，其范围遍及整个unFoo. 这意味着F a具有相同的范围。由于神奇的~超类约束，unFoo的签名等效于：

unfoo: Foo a -> F a

但这里是龙：F a不一定在任何地方都是格式良好的[第 3 节“总体陷阱”]，因为代码不需要证据存在适用的实例。

所以我完全不同意 dfeuer 的观点：FunDep 确实携带证据，就像Num b示例一样，并且该证据无法逃脱模式匹配；类型族F a不携带证据（实例匹配的证据——~约束在没有证据的情况下成立），因此F a在整个范围内可用a——“可用”并不意味着有效。