数据族vs内射型家族

问题描述

回顾过去关于数据族的StackOverflow问题，那里有一些关于数据族的问题是几年前讨论键入系列和数据系列，以及，了解数据族的使用情况。两者都表示，数据家族的注入是他们最大的优势。

查看，我看到不使用。

例如，假设我有一个数据族（我已经合并了文档中的一些示例，试图挤压数据族的所有功能）

 数据族G ab 
数据实例G Int Bool = G11 Int | G12 Bool派生（Eq）
新类型实例G（）a = G21 a 
数据实例G [a] b其中
 G31 :: c  - > G [Int] b 
 G32 :: G [a] Bool 
  

将其重写为

  type family G ab = g | g  - > ab 
类型实例G Int Bool = G_Int_Bool 
类型实例G（）a = G_Unit_a a 
类型实例G [a] b = G_lal_b ab 
 
 data G_Int_Bool = G11 Int | G12 Bool推导（Eq）
 newtype G_Unit_a a = G21 a 
 data G_lal_b a b其中
 G31 :: c  - > G_lal_b [Int] b 
 G32 :: G_lal_b [a] Bool 
  

数据族的相关实例以相同的方式对应于具有类型族的关联实例。那么剩下的唯一区别就是我们在类型命名空间中只有更少的东西？

作为后续，在类型命名空间中拥有更少的东西是否有益处？我能想到的是，这将成为调试地狱，因为有人在 ghci 上玩这个 - 构造函数的类型似乎都表明构造函数都在一个GADT下...

解决方案

  type family T a = r | r  - >一个
数据族D a 
  

一个内射类族 T 满足注入公理

但是数据族满足更强的生成性公理

你喜欢：因为 D 的实例定义了与任何现有类型不同的新类型。）

事实上 D 本身是类型系统中的一个合法类型，不像像 T 这样的类型族，它只能出现在一个完全饱和的应用程序，如 T a 。这意味着

• D 可以是另一个类型构造函数的参数，如 MaybeT D 。 （ MaybeT T 是不合法的。）

，例如实例Functor D 。 （你不能为类型族 Functor T 定义实例，无论如何它将无法使用，因为例如 map :: Functor f =>（a - > b） - > fa - > fb 依赖于类型 fa 确定 f 和 a ;为此工作 f 不能被允许根据类型族，甚至是内射型变化。）

Now that we have injective type families, is there any remaining use case for using data families over type families?

Looking at past StackOverflow questions about data families, there is this question from a couple years ago discussing the difference between type families and data families, and this answer about use cases of data families. Both say that the injectivity of data families is their greatest strength.

Looking at the docs on data families, I see reason not to rewrite all uses of data families using injective type families.

For example, say I have a data family (I've merged some examples from the docs to try to squeeze in all the features of data families)

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

I might as well rewrite it as

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

It goes without saying that associated instances for data families correspond to associated instances with type families in the same way. Then is the only remaining difference that we have less things in the type-namespace?

As a followup, is there any benefit to having less things in the type-namespace? All I can think of is that this will become debugging hell for someone playing with this on ghci - the types of the constructors all seem to indicate that the constructors are all under one GADT...

解决方案

type family T a = r | r -> a
data family D a

An injective type family T satisfies the injectivity axiom

But a data family satisfies the much stronger generativity axiom

(If you like: Because the instances of D define new types that are different from any existing types.)

In fact D itself is a legitimate type in the type system, unlike a type family like T, which can only ever appear in a fully saturated application like T a. This means

• D can be the argument to another type constructor, like MaybeT D. (MaybeT T is illegal.)

• You can define instances for D, like instance Functor D. (You can't define instances for a type family Functor T, and it would be unusable anyway because instance selection for, e.g., map :: Functor f => (a -> b) -> f a -> f b relies on the fact that from the type f a you can determine both f and a; for this to work f cannot be allowed to vary over type families, even injective ones.)

这篇关于数据族vs内射型家族的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！