对 GADT 和传播约束感到困惑

Question

有很多关于GADTs比 更好的问答DatatypeContexts，因为 GADT 会自动在正确的位置提供约束。例如这里，这里，这里。但有时似乎我仍然需要一个明确的约束。这是怎么回事？改编自此答案的示例：

{-# 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有一个Eq a约束藏在里面的GADTBag a。大概baz2'sEq a会想要已经存在的字典的副本（？）

GADT 是否可能有许多数据构造函数，每个构造函数都有不同的（或没有）约束？这不是这里的情况，或者对于受约束的数据结构（如包、集合、有序列表）的典型示例。

GADTBag使用DatatypeContextsinfers类型的数据类型的等效项baz与baz2.

奖金问题：为什么我不能得到一个普通的... deriving (Eq)for GADTBag？我可以得到一个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")

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

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

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

@leftroundabout 在您实际解构该x值之前，无法知道MkGADTBag构造函数确实适用。

是的：unGADTBag当且仅当在 上存在模式匹配时才定义字段标签MkGADTBag。（如果该类型有其他构造函数，情况可能会有所不同——尤其是那些也有 label 的构造函数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 的设计使得我们需要像x使用模式匹配一样手动要求评估 GADT 值。