这三者之间的差异是什么/为什么？ 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，如果有它会重叠。
ADDIT：澄清@ kabuhr的回答（谢谢）
与我认为您在部分问题中声称的相反，对于普通数据系列，在构造函数上进行匹配不会执行任何推理
这些类型很棘手，所以我希望我需要显式签名才能使用它们。在这种情况下，普通数据族最简单
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
正如你所说，神秘的“不可接触”的信息。我在“对那些构造函数进行匹配”评论中的意思是：编译器“知道”有效负载为Int（对于所有三个构造函数）的等式的rhs，因此您最好获得与此一致的任何签名。
然后我想data GADT a where ...好像data instance GADT a where ...。我可以给签名inferGADT :: GADT a -> a或inferGADT :: GADT Int -> Int（同样为inferFGADT）。这是有道理的：有一个data instance GADT a ...或我可以给一个更具体的类型的签名。
因此，在某些方面，数据系列是GADT的概括。我也像你说的那样看
因此，在某些方面，GADT是数据族的概括。
嗯。 （问题背后的原因是GHC Haskell已进入功能膨胀的阶段：有太多相似但不同的扩展。我试图将其修改为较少数量的底层抽象。然后@ HTNW的解释方法在进一步扩展方面与有助于学习者的方式相反。数据类型中的IMO存在性应该被淘汰：改为使用GADT。模式同义词应该用数据类型和它们之间的映射函数来解释，而不是相反。哦，还有一些DataKinds的东西，我在第一次阅读时跳过了。）
首先，您应该将数据系列视为碰巧由类型索引的独立ADT的集合，而GADT是具有可推断类型参数的单个数据类型，其中对该参数的约束（通常，等式约束） a ~ Int）可以通过模式匹配进入范围。
这意味着最大的区别在于，与我认为您在部分问题中声称的相反，对于普通数据系列，在构造函数上进行匹配不会对类型参数执行任何推断。特别是，这个类型检查：
inferGADT :: GADT a -> a
inferGADT (MkGADT n) = n
但这不是：
inferDF :: DF a -> a
inferDF (MkDF n) = n
并且没有类型签名，第一个将无法键入check（带有神秘的“不可触摸”消息），而第二个将被推断为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
您可以通过编写单独的构造函数块将其编写为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的基于模式的推理方法没有帮助的地方）。
如果我们对数据构造函数使用PatternSynonyms样式类型签名，我认为区别变得清晰。让我们从Haskell 98开始
data D a = D a a
你得到一个模式类型：
pattern D :: forall a. a -> a -> D a
它可以在两个方向阅读。 D，在“前进”或表达语境中说，“forall a，你可以给我2个as，我会给你一个D a”。 “向后”，作为一种模式，它说，“forall a，你可以给我一个D a，我会给你2 as”。
现在，您在GADT定义中编写的内容不是模式类型。这些是什么？谎言。谎言谎言。只有在替代方法是用ExistentialQuantification手动编写它们时才给予他们注意。我们来试试吧
data GD a where
GD :: Int -> GD Int
你得到
-- vv ignore
pattern GD :: forall a. () => (a ~ Int) => Int -> GD a
这说：forall a，你可以给我一个GD a，我可以给你一个证明a ~ Int，再加上Int。
重要观察：GADT构造函数的返回/匹配类型始终是“数据类型头”。我定义了data GD a where ...;我得到了GD :: forall a. ... GD a。对于Haskell 98构造函数以及data family构造函数也是如此，尽管它有点微妙。
如果我有一个GD a，我不知道a是什么，无论如何我都可以进入GD，即使我写了GD :: Int -> GD Int，这似乎说我只能与GD Ints匹配。这就是为什么我说GADT的构造者撒谎。模式类型永远不会存在。它清楚地表明，forall a，我可以将GD a与GD构造函数匹配，并获得a ~ Int和Int值的证据。
好的，data familys。不要让它们与GADT混合使用。
data Nat = Z | S Nat
data Vect (n :: Nat) (a :: Type) :: Type where
VNil :: Vect Z a
VCons :: a -> Vect n a -> Vect (S n) a -- try finding the pattern types for these btw
data family Rect (ns :: [Nat]) (a :: Type) :: Type
newtype instance Rect '[] a = RectNil a
newtype instance Rect (n : ns) a = RectCons (Vect n (Rect ns a))
现在实际上有两个数据类型头。正如@ K.A.Buhr所说，不同的data instances就像不同的数据类型一样，只是碰巧共享一个名字。模式类型是
pattern RectNil :: forall a. a -> Rect '[] a
pattern RectCons :: forall n ns a. Vect n (Rect ns a) -> Rect (n : ns) a
如果我有一个Rect ns a，我不知道ns是什么，我无法匹配它。 RectNil只接受Rect '[] as，RectCons只接受Rect (n : ns) as。你可能会问：“为什么我要降低功率呢？” @KABuhr给出了一个：GADT已关闭（并且有充分理由;敬请期待），家庭开放。这在Rect的情况下并不成立，因为这些实例已经填满了整个[Nat] * Type空间。原因实际上是newtype。
这是一个GADT RectG：
data RectG :: [Nat] -> Type -> Type where
RectGN :: a -> RectG '[] a
RectGC :: Vect n (RectG ns a) -> RectG (n : ns) a
我明白了
-- it's fine if you don't get these
pattern RectGN :: forall ns a. () => (ns ~ '[]) => a -> RectG ns a
pattern RectGC :: forall ns' a. forall n ns. (ns' ~ (n : ns)) =>
Vect n (RectG ns a) -> RectG ns' a
-- just note that they both have the same matched type
-- which means there needs to be a runtime distinguishment
如果我有一个RectG ns a并且不知道ns是什么，我仍然可以匹配就好了。编译器必须使用数据构造函数保留此信息。所以，如果我有一个RectG [1000, 1000] Int，我会产生一百万个RectGN构造函数的开销，这些构造函数都“保留”相同的“信息”。但是，Rect [1000, 1000] Int很好，因为我没有能力匹配并判断Rect是RectNil还是RectCons。这允许构造函数为newtype，因为它不包含任何信息。我会使用不同的GADT，有点像
data SingListNat :: [Nat] -> Type where
SLNN :: SingListNat '[]
SLNCZ :: SingListNat ns -> SingListNat (Z : ns)
SLNCS :: SingListNat (n : ns) -> SingListNat (S n : ns)
在Rect空间而不是O(sum ns)空间存储O(product ns)的尺寸（我认为这是正确的）。这也是GADTs关闭和家庭开放的原因。 GADT就像一个正常的data类型，除了它有平等证据和存在。将构造函数添加到GADT没有任何意义，只需将构造函数添加到Haskell 98类型是有意义的，因为任何不了解其中一个构造函数的代码都处于非常糟糕的时间。这对家庭来说很好，因为，正如您所注意到的，一旦您定义了一个家庭的分支，您就无法在该分支中添加更多构造函数。一旦你知道你所在的分支，就会知道构造函数，没有人可以破解它。如果您不知道要使用哪个分支，则不允许使用任何构造函数。
您的示例并不真正混合GADT和数据系列。模式类型很漂亮，因为它们规范了data定义中的表面差异，所以让我们来看看。
data family FGADT a
data instance FGADT a where
MkFGADT :: Int -> FGADT Int
给你
pattern MkFGADT :: forall a. () => (a ~ Int) => Int -> FGADT a
-- no different from a GADT; data family does nothing
但
data family DF a
data instance DF Int where
MkDF :: Int -> DF Int
给
pattern MkDF :: Int -> DF Int
-- GADT syntax did nothing
这是一个适当的混合
data family Map k :: Type -> Type
data instance Map Word8 :: Type -> Type where
MW8BitSet :: BitSet8 -> Map Word8 Bool
MW8General :: GeneralMap Word8 a -> Map Word8 a
这给出了模式
pattern MW8BitSet :: forall a. () => (a ~ Bool) => BitSet8 -> Map Word8 a
pattern MW8General :: forall a. GeneralMap Word8 a -> Map Word8 a
如果我有Map k v并且我不知道k是什么，我无法与MW8General或MW8BitSet匹配，因为那些只需要Map Word8s。这是data family的影响力。如果我有一个Map Word8 v并且我不知道v是什么，在构造函数上的匹配可以向我揭示它是否已知是Bool或者是其他东西。