不同之处: GADT、数据族、作为GADT的数据族
这三者之间的区别是什么/为什么？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 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就像你说的，神秘的“不可触及”的信息。我在“匹配那些构造器”注释中的意思是:编译器在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的泛化。我也看到你说的
所以，在某些方面，GADT是数据族的泛化。
嗯。(这个问题背后的原因是GHC Haskell已经到了功能膨胀的阶段:有太多相似但不同的扩展。我试着把它修剪成更少的底层抽象。那么@HTNW解释进一步扩展的方法与帮助学习者的方法是相反的。应该丢弃数据类型中的IMO存在项:使用GADT代替。应该从数据类型和它们之间的映射函数的角度来解释PatternSynonyms，而不是相反。哦，还有一些DataKinds的东西，我在第一次阅读时就跳过了。)
回答 2
Stack Overflow用户
发布于 2018-09-17 23:00:36
首先，您应该将数据族视为恰好由类型索引的独立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类型，只需使用GADTs就可以在很大程度上模拟DFs。例如，如果您有一个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的基于模式的推理方法没有帮助)。
Stack Overflow用户
发布于 2018-09-18 01:12:52
我认为如果我们为数据构造函数使用PatternSynonyms-style类型签名，区别就会变得很明显。让我们从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，我给你两个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。对于Haskell98构造函数和data family构造函数也是如此，尽管这有点微妙。
如果我有一个GD a，但我不知道a是什么，我还是可以传入GD，即使我写了GD :: Int -> GD Int，这似乎说明我只能用GADT s匹配它，这就是为什么我说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 instance行为类似于不同的数据类型，只是碰巧共享一个名称。模式类型为
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)空间(我认为这是正确的)。这也是GADT关闭而族打开的原因。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 Word8。这就是data family的影响。如果我有一个Map Word8 v，但我不知道v是什么，那么匹配构造函数可以告诉我它是Bool还是别的什么。
https://stackoverflow.com/questions/52367608
复制相似问题