Difference between type family and partial newtype? (and partial data?)

Question

I've had to interface two libraries where metadata is represented as a type parameter in one and as a record field in the other. I wrote an adaptor using a GADT. Here's a distilled version:

{-# LANGUAGE GADTs #-}

newtype TFId  a = MkId   a
data    TFDup a = MkDup !a !a

data GADT tf where
  ConstructorId  :: GADT TFId
  ConstructorDup :: GADT TFDup

main = do
  f ConstructorId
  f ConstructorDup

f :: GADT tf -> IO ()
f = _

This works. (May not be perfect; comments welcome, but that's not the question.)

It took me some time to get to this working state. My initial intuition was to use a type family for TFId, figuring: “GADT has kind (* -> *) -> *; in ConstructorDup TFDup has kind * -> *; so for ConstructorId I can use the following * -> * type family:”

{-# LANGUAGE TypeFamilies #-}
type family TFId a where TFId a = a

The type constructor does have the same kind * -> *, but GHC apparently won't have it in the same place:

error: …

The type family ‘TFId’ should have 1 argument, but has been given none

In the definition of data constructor ‘ConstructorId’ In the data type declaration for ‘GADT’

Well, if it says so…

I'm no sure I understand why it would make such a difference. No using type family stems without applying them? What's going on? Any other (better) way to do?

Yes, type families must be used saturated - that is, you have to apply the type family to all of its declared arguments. Type families are expanded at compile time, so the compiler has to know all of the type family's arguments in order to know what it's meant to expand into. The same applies to type synonyms. — Benjamin Hodgson
I'd be tempted to argue that newtypes are expanded (well, reduced) at compile-time as well, yet with them it works. So perhaps "compile-time" is a bit broad. What makes them different? In a word: why? — JB.
Sure, I was using the term "compile time" a bit loosely. newtypes are erased during code generation - the runtime representation of a newtype is the same as the wrapped type and it's free to coerce in either direction - but they are not expanded during type checking like types are. newtypes are apart from any other type; type synonyms/families are not. — Benjamin Hodgson
You could use a data family though, if you wanted. They're like type families but injective. — luqui
Thanks for the suggestion! As target types I've currently got a newtype (not pictured here), a data (that Dup) and a raw Int (the one I'm currently using my TFId functor for), so I'd have to convince myself Int is data, and compatible with whatever f does. Will give it a try. — JB.

chi chi · Accepted Answer · 2017-09-08T08:26:13

Injectivity.

type family F :: * -> *
type instance F Int  = Bool
type instance F Char = Bool

here F Int ~ F Char. However,

data G (a :: *) = ...

will never cause G Int ~ G Char. These are guaranteed to be distinct types.

In universal quantifications like

foo :: forall f a. f a -> a

f is allowed to be G (injective) but not allowed to be F (not injective).

This is to make inference work. foo (... :: G Int) can be inferred to have type Int. foo (... :: F Int) is equivalent to foo (... :: Bool) which may have type Int, or type Char -- it's an ambiguous type.

Also consider foo True. We can't expect GHC to choose f ~ F, a ~ Int (or Char) for us. This would involve looking at all type families and see if Bool can be produced by any on them -- essentially, we would need to invert all the type families. Even if this were feasible, it would generate a huge amount of possible solutions, so it would be ambiguous.

Difference between type family and partial newtype? (and partial data?)

1 Answers