haskell - 差异 : GADT, 数据族，数据族即 GADT

Question

这三者之间有什么/为什么有区别？ GADT(和常规数据类型)只是数据系列的简写吗？具体有什么区别:

data GADT a  where
  MkGADT :: Int -> GADT Int

data family FGADT a
data instance FGADT a  where             -- note not FGADT Int
  MkFGADT :: Int -> FGADT Int

data family DF a
data instance DF Int  where              -- using GADT syntax, but not a GADT
  MkDF :: Int -> DF Int

(这些例子是否过于简化，所以我没有看到差异的微妙之处？)

数据系列是可扩展的，但 GADT 不是。 OTOH 数据系列实例不得重叠。所以我不能为 FGADT 声明另一个实例/任何其他构造函数;就像我不能为 GADT 声明任何其他构造函数一样.我可以为 DF 声明其他实例.

通过对这些构造函数进行模式匹配，等式的 rhs 确实“知道”有效负载是 Int .

对于类实例(我很惊讶地发现)，我可以编写重叠实例来使用 GADT:

instance C (GADT a) ...
instance {-# OVERLAPPING #-} C (GADT Int) ...

(FGADT a), (FGADT Int) 也是如此.但不适用于 (DF a) : 必须是 (DF Int) - 那讲得通;没有 data instance DF a ，如果有它会重叠。

添加:澄清@kabuhr的回答(谢谢)

contrary to what I think you're claiming in part of your question, for a plain data family, matching on a constructor does not perform any inference

这些类型很棘手，所以我希望我需要明确的签名才能使用它们。在这种情况下，普通数据系列是最简单的

inferDF (MkDF x) = x                 -- works without a signature

推断类型 inferDF :: DF Int -> Int说得通。给它一个签名 inferDF :: DF a -> a没有意义:没有声明 data instance DF a ... .与 foodouble :: Foo Char a -> a 类似没有 data instance Foo Char a ... .

GADT 很尴尬，我已经知道了。因此，如果没有明确的签名，这些都不起作用

inferGADT (MkGADT x) = x
inferFGADT (MkFGADT x) = x

正如你所说，神秘的“不可触碰”的信息。我在“匹配那些构造函数”评论中的意思是:编译器“知道”一个方程的 rhs 有效载荷是 Int (对于所有三个构造函数)，所以你最好得到任何与之一致的签名。

然后我在想 data GADT a where ...好像 data instance GADT a where ... .我可以给个签名 inferGADT :: GADT a -> a或 inferGADT :: GADT Int -> Int (同样适用于 inferFGADT )。这是有道理的:有一个 data instance GADT a ...或者我可以在更具体的类型上签名。

因此，在某些方面，数据族是 GADT 的概括。我也看到你说的

So, in some ways, GADTs are generalizations of data families.

唔。 (问题背后的原因是 GHC Haskell 已经到了功能膨胀的阶段:有太多相似但不同的扩展。我试图将其精简为较少数量的底层抽象。然后@HTNW 的解释方法就进一步的扩展而言，这与对学习者的帮助相反。应该抛弃数据类型中的 IMO 存在主义:改用 GADT。PatternSynonyms 应该根据数据类型和它们之间的映射函数来解释，而不是相反。哦，还有一些 DataKinds 的东西，我在第一次阅读时跳过了。)

Answer 1

首先，您应该将数据族视为碰巧按类型索引的独立 ADT 的集合，而 GADT 是具有可推断类型参数的单一数据类型，其中对该参数的约束(通常是等式约束，例如a ~ Int ) 可以通过模式匹配纳入范围。

这意味着最大的区别在于，与我认为您在部分问题中所声称的相反，对于普通数据系列，构造函数上的匹配确实 不是 对类型参数执行任何推断。特别是，这个类型检查:

inferGADT :: GADT a -> a
inferGADT (MkGADT n) = n

但这不会:

inferDF :: DF a -> a
inferDF (MkDF n) = n

如果没有类型签名，第一个将无法进行类型检查(带有神秘的“不可触碰”消息)，而第二个将被推断为 DF Int -> Int .

对于像您的 FGADT 这样的情况，情况变得更加困惑。将数据系列与 GADT 相结合的类型，我承认我并没有真正考虑过它是如何工作的。但是，作为一个有趣的例子，考虑:

data family Foo a b
data instance Foo Int a where
  Bar :: Double -> Foo Int Double
  Baz :: String -> Foo Int String
data instance Foo Char Double where
  Quux :: Double -> Foo Char Double
data instance Foo Char String where
  Zlorf :: String -> Foo Char String

在这种情况下， Foo Int a是具有可推断 a 的 GADT范围:

fooint :: Foo Int a -> a
fooint (Bar x) = x + 1.0
fooint (Baz x) = x ++ "ish"

但是 Foo Char a只是单独 ADT 的集合，因此不会进行类型检查:

foodouble :: Foo Char a -> a
foodouble (Quux x) = x

出于同样的原因 inferDF不会在上面进行类型检查。

现在，回到你的平原 DF和 GADT类型，您可以在很大程度上模仿 DFs只使用 GADTs .例如，如果你有一个 DF:

data family MyDF a
data instance MyDF Int where
  IntLit :: Int -> MyDF Int
  IntAdd :: MyDF Int -> MyDF Int -> MyDF Int
data instance MyDF Bool where
  Positive :: MyDF Int -> MyDF Bool

您只需编写单独的构造函数 block 即可将其编写为 GADT:

data MyGADT a where
  -- MyGADT Int
  IntLit' :: Int -> MyGADT Int
  IntAdd' :: MyGADT Int -> MyGADT Int -> MyGADT Int
  -- MyGADT Bool
  Positive' :: MyGADT Int -> MyGADT Bool

因此，在某些方面，GADT 是数据系列的概括。但是，数据族的一个主要用例是为类定义关联的数据类型:

class MyClass a where
  data family MyRep a
instance MyClass Int where
  data instance MyRep Int = ...
instance MyClass String where
  data instance MyRep String = ...

需要数据系列的“开放”性质的地方(以及 GADT 基于模式的推理方法没有帮助的地方)。