haskell - Data families vs Injective type families

Question

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

Answer 1

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

An injective type family T satisfies the injectivity axiom

if T a ~ T b then a ~ b

But a data family satisfies the much stronger generativity axiom

if D a ~ g b then D ~ g and a ~ b

(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.)