Случаи использования семей данных

Ответ 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 имеет несколько различных видов векторов: вложенные векторы, распакованные векторы, примитивные векторы, сохраняемые векторы. Для каждого типа 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 всегда называется Mutable Vector: это ее имя, и у нее нет другого. Если у вас есть Mutable Vector, вы можете получить тип соответствующего неизменяемого vector, потому что он находится там как аргумент типа. С type family Mutable, как только вы примените его к аргументу, он будет оценивать неопределенный тип результата (предположительно называемый MVector, но вы не можете знать), и у вас нет способа отобразить обратную сторону.