数据系列用例

Question

使用类型同义词系列的好处很明显 - 它是类型级函数.

但数据系列并非如此- 所以我的问题是,数据系列的用例是什么？我应该在哪里使用它？

Answer 1

一个好处是数据系列是单射的,与类型系列不同.

如果你有

type family TF a
data family DF a

然后你知道这DF a ~ DF b意味着a ~ b,虽然使用TF,你不会 - 因为任何a你可以确定这DF a是一个全新的类型(就像[a]是一个不同的类型[b],当然,除非a ~ b),而类型系列可以映射多个将类型输入到同一现有类型.

第二个是数据族可以像任何其他类型构造函数一样部分应用,而类型族不能.

这不是一个特别真实的例子,但是例如,您可以这样做:

data instance DF Int    = DInt    Int
data instance DF String = DString String

class C t where
    foo :: t Int -> t String

instance C DF where -- notice we are using DF without an argument
                    -- notice also that you can write instances for data families at all,
                    -- unlike type families
    foo (DInt i) = DString (show i)

基本上,DF和DF a在实际的,一流的,合法的类型,对自己,像任何其他类型的声明用data.TF a只是一个评估类型的中间形式.

但是,当我想知道数据系列并阅读类似的东西时,我想所有这些都不是很有启发性,或者至少不适合我.

这是我经历的经验法则.每当你发现自己重复了你有一个类型族的模式,并且对于每种输入类型,你都要data为要映射的类型族声明一个新类型,那么切断中间人并使用数据族就更好了.

来自矢量库的真实示例.vector有几种不同的矢量:盒装矢量,无盒装矢量,原始矢量,可存储矢量.对于每种Vector类型,存在对应的可变MVector类型(法线向量是不可变的).所以它看起来像这样:

type family Mutable v :: * -> * -> * -- the result type has two type parameters

module Data.Vector{.Mutable} where
data Vector a = ...
data MVector s a = ...
type instance Mutable Vector = MVector

module Data.Vector.Storable{.Mutable} where
data Vector a = ...
data MVector s a = ...
type instance Mutable Vector = MVector

[etc.]

现在而不是那样,我宁愿:

data family Mutable v :: * -> * -> *

module Data.Vector{.Mutable} where
data Vector a = ...
data instance Mutable Vector s a = ...
type MVector = Mutable Vector

module Data.Vector.Storable{.Mutable} where
data Vector a = ...
data instance Mutable Vector s a = ...
type MVector = Mutable Vector

[etc.]

其中编码不变量,对于每种Vector类型,只有一种Mutable Vector类型,并且它们之间存在一对一的对应关系.Vector总是调用a的可变版本Mutable Vector:这是它的名字,它没有其他名称.如果你有一个Mutable Vector,你可以得到相应的不可变的类型Vector,因为它就像一个类型参数.有了type family Mutable,一旦你将它应用于一个参数,它就会计算出一个未指定的结果类型(可能被称为MVector,但你无法知道),并且你无法向后映射.