Support for type families, with defuntionalization
Here's a proposal to add support for data types that use type families in their fields.
This is a refinement of the "obvious" approach, using singletons or first-class-families, to avoid some extra issues if done naively. Familiarity with defunctionalization using either of those libraries is assumed in the rest of this post.
Problem 1: every type family must be associated with a defunctionalization symbol.
When we derive GenericK
we can generate defunctionalization symbols on the spot. We also don't need to defunctionalize families not mentioned in the generic data type, even if they are used indirectly.
Problem 2: doing so naively, by declaring new data
, may pollute the type namespace quite badly.
Type families, like every identifier, are identified by their source (module and name, and maybe package), so we can use the identifier (a string) as a defunctionalization symbol.
Step 0: defunctionalization with only one constructor (and lots of strings)
Here are core definitions for the kind of defunctionalization symbols and the open type family for evaluating them from first-class-instances; singletons should work as well. Crucially, we won't need the bazillion instances from either singletons or first-class-families. I would put this in a package fcf-core to enable reuse with first-class-families.
type family EvalI (e :: Exp k) :: k -- EvalI following naming scheme of ForAllI and SuchThatI
type Exp :: Type -> Type
type Exp k = Const Void k -> Type -- doesn't matter as long as it's Type at the end
The key addition from this proposal is a universal constructor for defunctionalization symbols Family
, indexed by the name of a type family. It's also useful to make the kind precise (dependent on the family) to accomodate the somewhat unintuitive matching semantics of type families.
type String = Symbol
data family Family_ (name :: String) :: k -- This is just to get a matchable type constructor, it won't actually have data instances.
type Family :: forall (name :: String) -> FamilyKind name -- getting a more precise kind
type Family name = Family_ name
type family FamilyKind (name :: String) :: Type
Atom
with a constructor to evaluate applied type families.
Step 1: in kind-apply, extend data Atom d k where
...
Eval :: Atom d (Exp k) -> Atom d k
type instance Interpret (Eval a) x = EvalI (Interpret a x)
When one defines a GenericK
instance for a type involving type families, they associate the name of each family to:
- its kind via
FamilyKind
, being careful to insert anExp
to mark the arity of the family; - the actual family via
EvalI
.
-- Example for (+) :: Nat -> Nat -> Nat
type instance FamilyKind "GHC.TypeNats.+" = Nat -> Nat -> Exp Nat
type instance EvalI (Family_ "GHC.TypeNats.+" m n) = m + n
Step 3. Implement that recipe in TH
Voilà.
Comments
-
If two data types use the same type family, their
deriveGenericK
will declare duplicatetype instance
, which is legal Haskell. -
This doesn't (yet) handle polykinded families. The problem is how to define their kind with
FamilyKind
, which can only be a monokind.type instance FamilyKind "Data.Type.Bool.If" = forall k. Bool -> k -> k -> k -- not allowed
-
Instead of the
data family Family_
trick to get a variadic matchable symbol, a simpler encoding may be to pack the arguments of a type family as a tuple.