在GADT中绑定时，功能依赖关系不统一

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基金会和GADT之间的互动。。。现在看起来很糟糕。

我认为这比这更重要(不仅仅是"此刻"，也不仅仅是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仅在匹配中有效。

附加：(针对评论(

为了扩展"；仅在(Foo x)〃上的匹配内的RHS上有效：

• 一般来说，GADT有许多构造函数，每个构造函数可能都有不同的约束
• (事实上，我们可能有一个没有构造函数的值，如(undefined :: Foo t)。(
• 因此，匹配必须在应用"仅在RHS上有效"的内容之前查看构造函数

出于这些目的，FunDep被视为任何其他约束，因此OP的问题类似于FooN的情况。(存在的b仅在RHS上起作用。(

@dfeuer使用类型族的重新设计不依赖于tyvarb的作用域；类型族适用于在整个unFoo中具有范围的a。这意味着F a具有相同的范围。由于神奇的~超类约束，unFoo的签名等价于：

unfoo: Foo a -> F a

但这里有龙：F a不一定在任何地方都形成得很好[第3节"Totality Trap"]，因为代码不需要证据证明存在适用的实例。

因此，我完全不同意dfeuer的观点：FunDep确实携带证据，就像Num b的例子一样，而且证据无法逃脱模式匹配；类型族F a不携带证据(实例匹配的证据——~约束在没有证据的情况下被保持(，因此F a在整个a-；可用"；并不意味着有效。