The family of type families

fcf-family promotes regular type families to first-class families without requiring new symbols that pollute the type namespace nor a centralized organization to decide where the symbol for each family should be defined.

All we need is a single symbol Family indexed by a qualified name that uniquely identifies an existing type family: package, module, and base name.

Example names:

-- GHC.TypeNats.+
MkName "base" "GHC.TypeNats" "+"

-- Data.Type.Bool.If
MkName "base" "Data.Type.Bool" "If"

Promoting a type family to first-class

For example, the type family (+) is promoted using the following Eval instance for Family:

type (::+) = MkName "base" "GHC.TypeNats" "+" -- Name of (+)
type instance Eval (Family_ (::+) _ '(x, '(y, '())))) = x + y

The necessary instances can be generated using fcfify from the module Fcf.Family.TH.

fcfify ''+

The name of the family can be quoted using familyName.

type (::+) = $(pure (familyName ''+))

Two modules may invoke fcfify on the same name without conflict. Identical type family instances will be generated, which is allowed.

Examples:

2 + 3
~
Eval (Family (MkName "base" "GHC.TypeNats" "+") P0 '(2, '(3, '())))

If a b c
~
Eval (Family (MkName "base" "Data.Type.Bool" "If") P1 '(a, '(b, '(c, ()))))

Details

The type of Family is an uncurried version of the original type family:

Family (::+) _ :: (Nat, (Nat, ())) -> Exp Nat
(+) :: Nat -> Nat -> Nat

Tuples (,) and () are used as the cons and nil of heterogeneous lists of arguments.

The signature of the relevant family is encoded by implementing the following type instances:

-- Auxiliary instances.
type instance Params (::+) = ()
type instance Args_ (::+) _ = (Nat, (Nat, ()))
type instance Res_ (::+) _ _ = Nat

Args_ and Res_ denote the types of arguments and result of the given type family. Params denotes the type of implicit parameters (there are none here since (+) is monomorphic). The type of explicit arguments (Args_) may depend on the implicit parameters (Params). The result type (Res_) may depend on both Params and Args_.

Untyped inside, typed outside

These families are intended to be very dependent (the type of Family depends on Res depends on Args depends on Params). However, the implementation of this library must work around some technical limitations of GHC. Args_ and Res_ are actually "untyped" to make GHC more lenient in type checking their instances. "Typed" wrappers, Family, Res, Args are then provided to invoke those families with their intended types, which allows type inference to work.

To recap: define instances of Params, Args_, Res_, Family_, but to invoke the latter three, use Args, Res, and Family instead.

Implicit parameters

An example using implicit parameters is If :: forall k. Bool -> k -> k -> k.

type If_ = MkName "base" "Data.Type.Bool" "If"
type instance Eval (Family_ If_ _ '(b, '(x, '(y, '())))) = If b x y

type instance Params If_ = (Type, ())  -- Type of the implicit parameter
type instance Args_ If_ k = (Bool, (k, (k, ())      -- Types of the explicit arguments
type instance Res_ If_ k _ = k                      -- Type of the result

The second argument of Family_ is a proxy that carries the implicit parameters in its type. For example, the type of Family If_ is really:

Family If_ (_ :: Proxy k) :: (Bool, (k, (k, ()))) -> k

When using Family, apply it to a proxy encoding the number of implicit parameters in unary using P0 and PS.

For example, use P0 for the monomorphic (+) and P1 (equal to PS P0) for If.

Reexported from first-class-families.

Parameters should be collected in a heterogeneous list made of () and (,).

• 0: ()
• 1: (a, ())
• 2: (a, (b, ()))
• 3: (a, (b, (c, ())))
• etc.

We want implicit parameters of polykinded type families to remain implicit in their promotion.

In Family, the parameters are collected in a tuple. To help type inference when using a promoted type family, we instantiate the spine of the tuple using the following proxies.

These coercions are part of hacks to work around some limitations in GHC.