时间戳

首页 > 解决方案 > 对 GADT 和传播约束感到困惑

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

问题描述

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在道德上是等价的，但有不同的类型。大概是因为unGADTBaghas no Eq a，那么约束不能传播到任何使用unGADTBag.

但是baz2有一个Eq a约束隐藏在GADTBag a. 大概baz2'sEq a会想要字典的副本已经存在（？）

GADT 是否可能有许多数据构造函数，每个构造函数都有不同（或没有）约束？这不是这里的情况，或者对于像 Bags、Sets、Ordered Lists 这样的受限数据结构的典型示例。

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来解释为什么它们有不同的类型？

标签： haskellgadt

解决方案

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

比较

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 值。

推荐阅读