数据族vs内射型家族
既然我们有内射类型族，那么在类型族中使用数据族还有什么用例吗？
回顾过去关于数据族的StackOverflow问题，几年前有一个问题讨论类型族和数据族之间的区别，以及关于数据族用例的这个答案。 两者都表示数据家族的注入是他们最大的优势。
查看数据族的文档，我发现不应该使用内射类族重写数据族的所有用途。
例如，假设我有一个数据族（我已经合并了文档中的一些示例，试图挤压数据族的所有功能）
data family G a b
data instance G Int Bool = G11 Int | G12 Bool deriving (Eq)
newtype instance G () a = G21 a
data instance G [a] b where
G31 :: c -> G [Int] b
G32 :: G [a] Bool
我不如将其重写为
type family G a b = g | g -> a b
type instance G Int Bool = G_Int_Bool
type instance G () a = G_Unit_a a
type instance G [a] b = G_lal_b a b
data G_Int_Bool = G11 Int | G12 Bool deriving (Eq)
newtype G_Unit_a a = G21 a
data G_lal_b a b where
G31 :: c -> G_lal_b [Int] b
G32 :: G_lal_b [a] Bool
不言而喻，数据族的相关实例以相同的方式对应于具有类型族的相关实例。 那么剩下的唯一区别就是我们在类型名称空间中的东西少了吗？
作为后续，在类型命名空间中拥有更少的东西是否有益处？ 我所能想到的是，这将成为调试地狱，因为有人在ghci上玩这个 - 构造函数的类型似乎都表明构造函数都在一个GADT下。
type family T a = r | r -> a
data family D a
一个内射型族T满足注入公理
如果T a ~ T b那么a ~ b
但是一个数据族满足了更强大的生成公理
如果D a ~ gb然后D ~ g和a ~ b
（如果您喜欢：因为D的实例定义了与现有类型不同的新类型。）
事实上D本身是类型系统中的一种合法类型，与像T这样的类型家族不同，它只能出现在像T a这样完全饱和的应用程序中。 意即
D可以是另一个类型构造函数的参数，如MaybeT D （ MaybeT T是非法的。）
您可以为D定义实例，如instance Functor D （你不能为类型族Functor T定义实例，无论如何它将无法使用，因为例如map :: Functor f => (a -> b) -> fa -> fb实例选择依赖于事实从fa类型你可以确定f和a ;为了这个工作f不能被允许改变类型族，甚至是内射型）。
您错过了另一个细节 - 数据族创建新类型。 类型系列只能引用其他类型。 特别是，数据族的每个实例都声明新的构造函数。 它很好通用。 如果你想要newtype语义，你可以用newtype instance创建一个数据实例。 你的实例可以是一个记录。 它可以有多个构造函数。 如果你愿意，它甚至可以成为GADT。
这是完全的区别type和data / newtype关键字。 内射型家族不会给你新的类型，在你需要的情况下使它们无用。
我明白你来自哪里。 最初我对这个差异有同样的问题。 然后，我终于遇到了一个用例，他们很有用，即使没有参与类型课程。
我想在不使用类的情况下编写一个在几个不同的上下文中处理可变单元格的api。 我知道我想用一个免费的monad来解决IO ， ST口译员问题，也许有些可怕的黑客用unsafeCoerce甚至把它塞进State 。 当然，这并不是出于任何实际目的 - 我只是在探索API设计。
所以我有这样的东西：
data MutableEnv (s :: k) a ...
newRef :: a -> MutableEnv s (Ref s a)
readRef :: Ref s a -> MutableEnv s a
writeRef :: Ref s a -> a -> MutableEnv s ()
MutableEnv的定义并不重要。 只是标准的免费/操作monad的东西与构造函数匹配在API中的三个功能。
但我被卡在什么来定义参考。 就类型系统而言，我不想要某种类，我希望它是一个具体类型。
然后，一天晚上我出去散步，它打到了我 - 我基本上想要的是一个类型，它的构造函数被一个参数类型索引。 但它必须是开放的，与GADT不同 - 新的口译员可以随意添加。 然后它就撞到了我。 这正是数据家族的特征。 一个开放的，类型索引的数据值家族。 我可以用以下方法完成api：
data family Ref (s :: k) :: * -> *
然后，处理Ref的底层代表并不是什么大问题。 只要定义了MutableEnv的解释器，就可以创建一个数据实例（或者更可能是MutableEnv实例）。
这个确切的例子并不是很有用。 但它清楚地说明了数据族可以做的事情，即内射型家族无法做到的事情。
里德巴顿的答案完美地解释了我的两个例子之间的区别。 它让我想起了我在Richard Eisenberg关于向Haskell添加依赖类型的论文中读到的一些东西，我认为既然这个问题的核心是注入性和生成性，那么值得一提的是DependentHaskell将如何处理这个问题（当它最终得到实现时，如果现在提出的量词是最终实施的量词）。
以下是基于上述论文的第56和57页（4.3.4匹配性）
定义 （生成性） 。 如果f和g是生成，然后fa ~ gb意味着f ~ g
定义 （注入） 。 如果f是单射，然后fa ~ fb意味着a ~ b
定义 （Matchability） 。 函数f是可匹配的，如果它是生成的和内射的
在Haskell中，我们现在知道它（8.0.1），可匹配的（类型级别）函数完全由新类型，数据和数据族类型构造函数组成。 在将来，在DependentHaskell下，我们将得到的新量词之一将是'->并且这将用于表示可匹配的函数。 换句话说，有一种方法可以告诉编译器一个类型级别的函数是生成的（目前只能通过确保该函数是一个类型构造函数来完成）。