haskell - familias de datos casos de uso

type-families

Question

Los beneficios de usar familias de sinónimos de tipo son claros: son funciones de nivel de tipo.

Pero no es el caso de las familias de datos , por lo que mi pregunta es: ¿qué son los casos de uso para las familias de datos? ¿Dónde debería usarlo?

Answer 1

Un beneficio es que las familias de datos son inyectivas, a diferencia de las familias de tipos.

Si usted tiene

type family TF a
data family DF a

Entonces sabe que DF a ~ DF b implica que a ~ b , mientras que con TF, no lo hace; para cualquier a , puede estar seguro de que DF a es un tipo completamente nuevo (al igual que [a] es un tipo diferente desde [b] , a menos que por supuesto a ~ b ), mientras que una familia de tipos puede asignar múltiples tipos de entrada al mismo tipo existente.

Una segunda es que las familias de datos se pueden aplicar parcialmente, como cualquier otro constructor de tipo, mientras que las familias de tipo no se pueden aplicar.

Este no es un ejemplo particularmente del mundo real, pero por ejemplo, puede hacer:

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)

Básicamente, DF y DF a son reales, de primera clase, tipos legítimos, en sí mismos, como cualquier otro tipo que declara con data . TF a es solo una forma intermedia que se evalúa a un tipo.

Pero supongo que todo eso no es muy esclarecedor, o al menos no lo fue para mí, cuando me preguntaba acerca de las familias de datos y leía cosas similares.

Aquí está la regla de oro que paso. Cuando te encuentras repitiendo el patrón en el que tienes una familia de tipos, y para cada tipo de entrada, declaras un nuevo tipo de data para la familia de tipos para mapear, es mejor cortar el intermediario y usar una familia de datos en su lugar.

Un ejemplo del mundo real de la biblioteca de vector . vector tiene varios tipos diferentes de vectores: vectores en caja, vectores sin caja, vectores primitivos, vectores almacenables. Para cada tipo de Vector hay un tipo de MVector mutable MVector (los Vectores normales son inmutables). Así que se ve así:

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.]

Ahora en lugar de eso, prefiero tener:

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.]

Lo que codifica el invariante de que para cada tipo de Vector hay exactamente un tipo de Mutable Vector , y que hay una correspondencia de uno a uno entre ellos. La versión mutable de un Vector siempre se llama Mutable Vector : ese es su nombre y no tiene otro. Si tiene un Mutable Vector , puede obtener el tipo del Vector inmutable correspondiente, porque está ahí como un argumento de tipo. Con el type family Mutable , una vez que lo aplique a un argumento, éste se evalúa a un tipo de resultado no especificado (presumiblemente llamado MVector , pero no puede saberlo), y no tiene forma de mapear hacia atrás.