对 GADT 和传播约束感到困惑

Question

有很多关于 GADTs 比 DatatypeContexts 更好的问答，因为 GADT 会自动在正确的位置提供约束。例如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，Eq a 约束隐藏在GADTBag 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 中执行的代码，如果相关的话。）

Addit: 根据@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)) arising from a use of ``MkGADTBag'/ ``baz2' 分别 [编辑： 我最初的 Addit 给出了错误的表达式和错误的错误信息]：

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

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

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

是的：当且仅当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。

Answer 2

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

在您实际解构 x 值之前，无法知道 MkGADTBag 构造函数确实适用。当然，如果没有，那么您还有其他问题（底部），但可以想象这些问题可能不会浮出水面。考虑

ignore :: a -> b -> b
ignore _ = id

baz2' :: GADTBag a -> Maybe [a] -> Bool
baz2' x y = ignore (unGADTBag x) (y==y)

请注意，我现在可以使用undefined :: GADTBag (Int->Int) 来调用该函数。应该不是问题，因为undefined 是ignored，对吧^★？问题是，尽管Int->Int 没有Eq 实例，但我能够编写y==y，而y :: Maybe [Int->Int] 实际上无法支持。

所以，我们不能只提及unGADTBag 足以将Eq a 约束注入其周围范围。相反，我们必须将该约束的范围明确界定为我们已确认 MkGADTBag 构造函数确实适用的地方，并且模式匹配完成了这一点。

---

^★_{如果您对我的论点依赖于undefined 感到恼火，请注意，当存在多个将不同约束带入范围的构造函数时也会出现同样的问题。子>}

---

另一种可行的模式匹配方法是：

{-# LANGUAGE RankNTypes #-}

withGADTBag :: GADTBag a -> (Eq a => [a] -> b) -> b
withGADTBag (MkGADTBag x) f = f x

baz3 :: GADTBag a -> Maybe [a] -> Bool
baz3 x y = withGADTBag x (== fromJust y)

---

对修改的回应

所有这些都给*** Exception: Prelude.undefined：

是的，他们当然会这样做，因为您实际上在函数中评估了x == y。因此，如果输入具有 NF，则该函数只能产生非⟂。但这绝不是所有函数的情况。

而这两个在编译时给出相同的类型错误

当然会这样做，因为您试图在 MkGADTBag 构造函数中包装非Eq 类型的值，这显式需要该约束（并允许您再次显式解包！），而GADTBag type 不需要该约束。 （这就是这种封装的重点！）

在您真正解构 x 值之前，无法知道 `MkGADTBag` 构造函数确实适用。

是的：当且仅当存在模式匹配时，才定义字段标签 `unGADTBag`在“MkGADTBag”上。

可以说，这是字段标签应该工作的方式，但在 Haskell 中它们不是。字段标签不过是从数据类型到字段类型的函数，如果有多个构造函数，则为 nontotal 函数。
是的，Haskell 记录是设计最差的记录之一语言的特点。我个人倾向于仅将字段标签用于大型、单一构造函数、普通旧数据类型（即使这样，我也更喜欢不直接使用字段标签，而是从它们派生的 lenses）。

无论如何，我看不到“如果存在模式匹配，则定义字段标签”甚至可以以允许您的代码按您认为应该的方式工作的方式实现。编译器必须在某处插入确认构造函数应用（并提取其 GADT 封装约束）的步骤。但是在哪里？在您的示例中，这是相当明显的，但一般来说，x 可能会占据一个具有许多决策分支的广阔范围，并且您真的不希望它在实际上不需要约束的分支中得到评估。

另外请记住，当我们与 undefined/⟂ 争论时，这不仅仅是关于实际发散的计算，更常见的是您担心计算会花费很长时间（只是，Haskell 实际上并不有“花很长时间”的概念）。

Answer 3

考虑这个问题的方法是OutsideIn(X) ... with local assumptions。这与不确定性或惰性评估无关。 GADT 构造函数上的模式匹配在外部，等式的 RHS 在内部。构造函数的约束仅在本地可用 - 仅在内部。

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

在外部有一个显式数据构造函数MkGADTBag，提供Eq a。 x == y 在本地/内部引发了一个通缉的Eq a，它从模式匹配中退出。 OTOH

baz2           x        y  = unGADTBag x == fromJust y

外部没有显式数据构造函数，因此不提供上下文。 unGADTBag 有一个 Eq a，但它在 l.h 内部更深。 == 的参数；类型推断不会深入内部。它只是没有。然后在unGADTBag的有效定义中

unGADTBag (MkGADTBag x) = x

有一个Eq a 可以从外部获得，但它不能从RHS 逃逸到unGADTBag 使用站点的类型环境中。它只是没有。伤心！

我能看到的最好的解释是在 OutsideIn 论文的结尾部分，9.7 强调主要类型是否合理？（一个反问但我的回答是：当然，我们必须强调主体类型；在某些情况下，类型推断可能会得到更好的主体性。）最后一节考虑了这个例子

    data R a where
      RInt :: Int -> R Int
      RBool :: Bool -> R Bool
      RChar :: Char -> R Char

    flop1 (RInt x) = x

有第三种类型可以说是更可取的 [for flop1]，这种类型是 R Int -> Int。

flop1 的定义与unGADTBag 的形式相同，其中a 被限制为Int。

    flop2 (RInt x) = x
    flop2 (RBool x) = x

不幸的是，普通的多态类型太弱了，无法表达这个限制[即a只能是Int或Bool]而我们只能得到Ɐa.R a -> a对于flop2，这不规则应用的 flop2 到 R Char 类型的值。

因此，在这一点上，论文似乎放弃了尝试改进更好的主体类型：

总之，放弃一些自然的主要类型，转而采用更专业的类型，在运行时消除更多的模式匹配错误是很有吸引力的，但除非我们考虑一种更具表现力的类型语法，否则它并不完全有效。此外，如何在高级声明性规范中指定这些类型也远非显而易见。

“很有吸引力”。它只是没有。

我可以看到一个通用的解决方案是困难的/不可能的。但是对于受约束的 Bags/Lists/Sets 的用例，规范是：

• 所有数据构造函数对数据类型的参数都有相同的约束。
• 所有构造函数都产生相同的类型（... -> T a 或 ... -> T [a] 或 ... -> T Int 等）。
• 具有单个构造函数的数据类型很容易满足这一点。

为了满足第一个要点，对于使用二叉平衡树的 Set 类型，Nil 构造函数的定义并不明显：

data OrdSet a  where
  SNode :: Ord a => OrdSet a -> a -> OrdSet a -> OrdSet a
  SNil  :: Ord a => OrdSet a                     -- seemingly redundant Ord constraint

即便如此，在每个节点和每个终端上重复约束似乎很浪费：它一直是相同的约束（这与 EDSL 抽象语法树的 GADT 不同）；大概每个节点都携带一份完全相同的字典。

确保每个构造函数都具有相同约束的最佳方法就是将约束添加到数据类型的前缀：

data Ord a => OrdSet a  where ...

也许约束可以“OutsideOut”到访问树的环境。

Answer 4

另一种可能的方法是将PatternSynonym 与an explicit signature giving a Required constraint 结合使用。

pattern EqGADTBag :: Eq a => [a] -> GADTBag a              -- that Eq a is the *Required*
pattern EqGADTBag{ unEqGADTBag } = MkGADTBag unEqGADTBag   -- without sig infers Eq a only as *Provided*

也就是说，没有那个显式的签名：

*> :i EqGADTBag
pattern EqGADTBag :: () => Eq a => [a] -> GADTBag a

() => Eq a => ... 显示 Eq a 已提供，由 GADT 构造函数产生。

现在我们都推断出baz, baz2 :: Eq a => GADTBag a -> Maybe [a] -> Bool：

baz (EqGADTBag x) (Just y) = x == y

baz2           x        y  = unEqGADTBag x == fromJust y

出于好奇：可以使用 GADT decl 中的名称为 baz, baz2 以及 O.P. 中的那些方程提供这些方程。 GHC [正确] 警告重叠模式；并确实推断出baz 的约束信号。

我想知道这里是否有设计模式？不要对数据构造函数施加约束——也就是说，不要让它成为 GADT。而是声明一个带有必需/提供约束的“影子”PatternSynonym。

Answer 5

您可以在折叠函数中捕获约束，(Eq a => ..) 表示您可以假设 Eq a 但只能在函数 next 内（在模式匹配后定义）。如果你实例化next as = fromJust maybe == as，它会使用这个约束来见证平等

--              local constraint 
--              |
--              vvvvvvvvvvvvvvvvvv
foldGADTBag :: (Eq a => [a] -> res) -> GADTBag a -> res
foldGADTBag next (MkGADTBag as) = next as

baz3 :: GADTBag a -> Maybe [a] -> Bool
baz3 gadtBag maybe = foldGADTBag (fromJust maybe ==) gadtBag

---

type Ty :: Type -> Type
data Ty a where
 TyInt  :: Int -> Ty Int
 TyUnit :: Ty ()

--         locally assume Int       locally assume unit
--         |                        |
--         vvvvvvvvvvvvvvvvvvv      vvvvvvvvvvvvv
foldTy :: (a ~ Int => a -> res) -> (a ~ () => res) -> (Ty a -> res)
foldTy int unit (TyInt i) = int i
foldTy int unit TyUnit    = unit

eval :: Ty a -> a
eval = foldTy id ()