haskell - 在 GADT 中绑定(bind)时功能依赖不统一

Question

在以下代码中:

class FD a b | a -> b

data Foo a where
  Foo :: FD a b => b -> Foo a

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

按照常识，这应该可行，因为 a GADT 和函数中的约束相同，它确定 b ，但是这不会编译并出现以下错误:

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

有什么好的理由让它不起作用吗？

Answer 1

@chi The interactions between fundeps and GADTs, ... seem pretty bad at the moment.

我认为它比这更重要(不仅仅是“目前”，也不仅仅是对于 FunDeps)。
无论编译器推断出 x 的类型，在

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's reworking使用类型族不依赖于 tyvar b 的范围;类型族适用于 a ，其范围遍及 unFoo .这意味着 F a具有相同的范围。因为魔法 ~父类(super class)约束， unFoo的签名等价于:

unfoo: Foo a -> F a

但这里是龙: F a is not necessarily well-formed everywhere [Section 3 'Totality Trap']，因为代码不需要证明存在适用的实例。
所以我完全不同意 dfeuer:FunDep 确实有证据，就像 Num b 一样。例如，证据无法逃脱模式匹配；类型族 F a不携带证据(实例匹配—— ~ 约束在没有证据的情况下被认为是成立的)，所以 F a可在 a 的整个范围内使用——“可用”并不意味着有效。