21

使用类型同义词族的好处很明显——它是类型级函数。

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

4

1 回答 1

23

一个好处是数据族是单射的，不像类型族。

如果你有

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类型的不变量，并且它们之间存在一对一的对应关系。a 的可变版本Vector总是被称为Mutable Vector: 这是它的名字，它没有别的名字。如果你有 a Mutable Vector，你可以获得对应的 immutable 的类型Vector，因为它作为类型参数就在那里。使用type family Mutable，一旦将其应用于参数，它就会评估为未指定的结果类型（大概称为MVector，但您不知道），并且您无法向后映射。

于 2013-01-07T13:25:27.953 回答