这三者之间的差异是什么/为什么？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
正如你所说,神秘的"不可接触"的信息.我在"对那些构造函数进行匹配"评论中的意思是:编译器"知道"有效负载的等式的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存在性应该被淘汰:使用GADTs.模式同义词应该用数据类型和它们之间的映射函数来解释,而不是相反.哦,还有一些DataKinds的东西,我在第一次阅读时跳过了.)
首先,您应该将数据系列视为碰巧由类型索引的独立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
您可以通过编写单独的构造函数块将其编写为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的基于模式的推理方法没有帮助的地方).