haskell - 对 GADT 和传播约束感到困惑

Question

有很多关于 GADTs 比 DatatypeContexts 更好的问答，因为 GADTs 会自动在正确的地方提供约束。例如here , here , here .但有时我似乎仍然需要一个明确的约束。这是怎么回事？示例改编自 this answer :

{-# LANGUAGE  GADTs  #-}
import Data.Maybe                                              -- fromJust

data GADTBag a  where
  MkGADTBag :: Eq a => { unGADTBag :: [a] } -> GADTBag a

baz (MkGADTBag x) (Just y) = x == y

baz2           x        y  = unGADTBag x == fromJust y


-- unGADTBag :: GADTBag a -> [a]                               -- inferred, no Eq a

-- baz ::          GADTBag a -> Maybe [a] -> Bool              -- inferred, no Eq a
-- baz2 :: Eq a => GADTBag a -> Maybe [a] -> Bool              -- inferred, with Eq a

为什么 unGADTBag 的类型不能告诉我们 Eq a？

baz 和 baz2 在道德上是等价的，但有不同的类型。大概是因为 unGADTBag 没有 Eq a，所以约束无法传播到使用 unGADTBag 的任何代码中。

但是对于 baz2，GADTBag a 中隐藏了一个 Eq a 约束。据推测，baz2 的 Eq a 将需要字典的副本(？)

GADT 是否可能有许多数据构造函数，每个构造函数都有不同(或没有)约束？这不是这里的情况，也不是典型的受约束数据结构示例，例如 Bags、Sets、Ordered Lists。

使用 DatatypeContexts 的 GADTBag 数据类型的等效项推断出 baz 的类型与 baz2 相同。

额外的问题:为什么我不能为 GADTBag 得到一个普通的 ... deriving (Eq)？我可以用 StandaloneDeriving 得到一个，但这很明显，为什么 GHC 不能为我做这件事？

deriving instance (Eq a) => Eq (GADTBag a)

问题又来了，可能还有其他数据构造函数？

(在 GHC 8.6.5 中执行的代码，如果相关的话。)

补充:根据@chi 和@leftroundabout 的回答——我认为这两个回答都没有说服力。所有这些都给出了 *** Exception: Prelude.undefined:

*DTContexts> unGADTBag undefined
*DTContexts> unGADTBag $ MkGADTBag undefined
*DTContexts> unGADTBag $ MkGADTBag (undefined :: String)
*DTContexts> unGADTBag $ MkGADTBag (undefined :: [a])

*DTContexts> baz undefined (Just "hello")
*DTContexts> baz (MkGADTBag undefined) (Just "hello")
*DTContexts> baz (MkGADTBag (undefined :: String)) (Just "hello")

*DTContexts> baz2 undefined (Just "hello")
*DTContexts> baz2 (MkGADTBag undefined) (Just "hello")
*DTContexts> baz2 (MkGADTBag (undefined :: String)) (Just "hello")

而这两个在编译时给出相同的类型错误 * Couldn't match expected type ``[Char]'* No instance for (Eq (Int -> Int)) 分别因使用 ``MkGADTBag'/ ``baz2' [编辑: 我最初的 Addit 给出了错误的表达式和错误的错误信息]:

*DTContexts> baz (MkGADTBag (undefined :: [Int -> Int])) (Just [(+ 1)])
*DTContexts> baz2 (MkGADTBag (undefined :: [Int -> Int])) (Just [(+ 1)])

所以 baz, baz2 在道德上是等价的，不仅仅是因为它们对相同的明确定义的参数返回相同的结果；但也因为它们对相同的定义不明确的参数表现出相同的行为。或者它们的区别仅在于报告缺少 Eq 实例的地方？

@leftroundabout Before you've actually deconstructed the x value, there's no way of knowing that the MkGADTBag constructor indeed applies.

是的，有:当且仅当 MkGADTBag 上有模式匹配时，字段标签 unGADTBag 才被定义。 (如果该类型有其他构造函数，情况可能会有所不同——特别是如果它们也有标签 unGADTBag。)同样，未定义/延迟评估不会推迟类型推断。

明确地说，“[不]令人信服”的意思是:我可以看到我得到的行为和推断类型。我没有看到懒惰或潜在的不确定性会妨碍类型推断。我怎样才能揭示 baz、baz2 之间的差异，从而解释为什么它们具有不同的类型？

Answer 1

函数调用永远不会在范围内带来类型类约束，只有(严格的)模式匹配才会。

比较

unGADTBag x == fromJust y

本质上是一个形式的函数调用

foo (unGADTBag x) (fromJust y)

foo 需要 Eq a。这在道德上由 unGADTBag x 提供，但该表达式尚未评估!由于惰性，unGADTBag x 将仅在(并且如果)foo 需要其第一个参数时进行评估。

因此，为了在此示例中调用 foo，我们需要提前评估其参数。虽然 Haskell 可以像这样工作，但这将是一个相当令人惊讶的语义，其中参数是否被评估取决于它们是否提供所需的类型类约束。想象更一般的情况，例如

foo (if cond then unGADTBag x else unGADTBag z) (fromJust y)

这里应该评估什么？ unGADTBag x? unGADTBag y?两个都？ cond 还有吗？很难说。

由于这些问题，Haskell 被设计成我们需要使用模式匹配手动要求评估 GADT 值，例如 x。