Fcf.Family

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.

Main definitions

First-class families

Reexported from first-class-families.

type Exp a = a -> Type

Kind of type-level expressions indexed by their result type.

type family Eval (e :: Exp a) :: a

Expression evaluator.

Instances

type Eval (NDFamily_ name proxy e args :: a -> Type)

Defined in Fcf.Family

type Eval (NDFamily_ name proxy e args :: a -> Type) = Transp e (Eval (Coerce (Family name proxy args) :: Exp (Res_ name ks (Any :: Args_ name ks))))

type Eval (Family_ ('MkName "fcf-family-0.2.0.0-DLmiXsHvx0GCGU0RCPpriE" "Fcf.Family" "Params") _1 '(name, '()) :: Type -> Type)

Defined in Fcf.Family.Meta

type Eval (Family_ ('MkName "fcf-family-0.2.0.0-DLmiXsHvx0GCGU0RCPpriE" "Fcf.Family" "Params") _1 '(name, '()) :: Type -> Type) = Params name

type Eval (Family_ ('MkName "first-class-families-0.8.0.1-JfHCz6LQaAuFge3ERI6pGg" "Fcf.Core" "Eval") _1 '(e, '()) :: a -> Type)

Defined in Fcf.Family.Meta

type Eval (Family_ ('MkName "first-class-families-0.8.0.1-JfHCz6LQaAuFge3ERI6pGg" "Fcf.Core" "Eval") _1 '(e, '()) :: a -> Type) = Eval e

Family of families

data Name

Qualified name of a type family or type synonym.

Constructors

MkName

Fields

• Symbol

  Package name

• Symbol

  Module name

• Symbol

  Type name

Instances

type Eval (Family_ ('MkName "fcf-family-0.2.0.0-DLmiXsHvx0GCGU0RCPpriE" "Fcf.Family" "Params") _1 '(name, '()) :: Type -> Type)

Defined in Fcf.Family.Meta

type Eval (Family_ ('MkName "fcf-family-0.2.0.0-DLmiXsHvx0GCGU0RCPpriE" "Fcf.Family" "Params") _1 '(name, '()) :: Type -> Type) = Params name

type Family name proxy args = Family_ name proxy args

A general defunctionalization symbol for promoted type families. It encodes saturated applications of type families.

The second argument (proxy :: ParamsProxy name ks) is a gadget carrying implicit parameters (if any). When invoking Family, it must be applied to a proxy that corresponds to its number of implicit parameters: P0, P1, P2, ..., P7, or a unary encoding using P0 and PS for larger implicit arities. (This really matters for arity 2 and more.)

Implementation note

This module makes heavy use of dependently typed type families. There is a longstanding issue which severely limits the usability of such families when done naively.

The workaround used here is to make the type families themselves "untyped", and wrap them within "typed" synonyms.

Making the families untyped makes GHC more lenient so that it accepts them. Making the wrappers typed recovers the type inference behavior of the original family. For instance, when using If, one would expect to unify the types of its two branches. That is the case when constructing its defunctionalization symbol using Family and not with Family_.

data Family_ :: Name -> Proxy ks -> args -> Exp res

Untyped internals of Family

Instances

type Eval (Family_ ('MkName "fcf-family-0.2.0.0-DLmiXsHvx0GCGU0RCPpriE" "Fcf.Family" "Params") _1 '(name, '()) :: Type -> Type)

Defined in Fcf.Family.Meta

type Eval (Family_ ('MkName "fcf-family-0.2.0.0-DLmiXsHvx0GCGU0RCPpriE" "Fcf.Family" "Params") _1 '(name, '()) :: Type -> Type) = Params name

type Eval (Family_ ('MkName "first-class-families-0.8.0.1-JfHCz6LQaAuFge3ERI6pGg" "Fcf.Core" "Eval") _1 '(e, '()) :: a -> Type)

Defined in Fcf.Family.Meta

type Eval (Family_ ('MkName "first-class-families-0.8.0.1-JfHCz6LQaAuFge3ERI6pGg" "Fcf.Core" "Eval") _1 '(e, '()) :: a -> Type) = Eval e

type NDFamily name proxy = NDFamily_ name proxy Refl

Non-dependently typed family.

data NDFamily_ :: forall (name :: Name) -> forall (ks :: Params name). ParamsProxy name ks -> (Res name ks Any :~: r) -> Args name ks -> Exp r

Untyped internals of NDFamily.

Instances

type Eval (NDFamily_ name proxy e args :: a -> Type)

Defined in Fcf.Family

type Eval (NDFamily_ name proxy e args :: a -> Type) = Transp e (Eval (Coerce (Family name proxy args) :: Exp (Res_ name ks (Any :: Args_ name ks))))

Encoding type family signatures

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

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

type family Params (name :: Name) :: Type

Type of implicit parameters of the named family.

Instances

type Params ('MkName "fcf-family-0.2.0.0-DLmiXsHvx0GCGU0RCPpriE" "Fcf.Family" "Params")

Defined in Fcf.Family.Meta

type Params ('MkName "fcf-family-0.2.0.0-DLmiXsHvx0GCGU0RCPpriE" "Fcf.Family" "Params") = ()

type Params ('MkName "first-class-families-0.8.0.1-JfHCz6LQaAuFge3ERI6pGg" "Fcf.Core" "Eval")

Defined in Fcf.Family.Meta

type Params ('MkName "first-class-families-0.8.0.1-JfHCz6LQaAuFge3ERI6pGg" "Fcf.Core" "Eval") = (Type, ())

type Args (name :: Name) (ks :: Params name) = Args_ name ks

Type of explicit parameters of the named family.

type family Args_ (name :: Name) (ks :: ksT) :: Type

Untyped internals of Args

Instances

type Args_ ('MkName "fcf-family-0.2.0.0-DLmiXsHvx0GCGU0RCPpriE" "Fcf.Family" "Params") '()

Defined in Fcf.Family.Meta

type Args_ ('MkName "fcf-family-0.2.0.0-DLmiXsHvx0GCGU0RCPpriE" "Fcf.Family" "Params") '() = (Name, ())

type Args_ ('MkName "first-class-families-0.8.0.1-JfHCz6LQaAuFge3ERI6pGg" "Fcf.Core" "Eval") ('(a, '()) :: (Type, ()))

Defined in Fcf.Family.Meta

type Args_ ('MkName "first-class-families-0.8.0.1-JfHCz6LQaAuFge3ERI6pGg" "Fcf.Core" "Eval") ('(a, '()) :: (Type, ())) = (Exp a, ())

type Res (name :: Name) (ks :: Params name) (args :: Args name ks) = Res_ name ks args

Type of result of the named family.

type family Res_ (name :: Name) (ks :: ksT) (args :: argsT) :: Type

Untyped internals of Res

Instances

type Res_ ('MkName "fcf-family-0.2.0.0-DLmiXsHvx0GCGU0RCPpriE" "Fcf.Family" "Params") '() (_1 :: argsT)

Defined in Fcf.Family.Meta

type Res_ ('MkName "fcf-family-0.2.0.0-DLmiXsHvx0GCGU0RCPpriE" "Fcf.Family" "Params") '() (_1 :: argsT) = Type

type Res_ ('MkName "first-class-families-0.8.0.1-JfHCz6LQaAuFge3ERI6pGg" "Fcf.Core" "Eval") ('(a, '()) :: (Type, ())) (_1 :: argsT)

Defined in Fcf.Family.Meta

type Res_ ('MkName "first-class-families-0.8.0.1-JfHCz6LQaAuFge3ERI6pGg" "Fcf.Core" "Eval") ('(a, '()) :: (Type, ())) (_1 :: argsT) = a

Implicit parameters

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.

type ParamsProxy (name :: Name) (ks :: Params name) = Proxy ks

Synonym to make explicit the dependency of the type of the implicit parameters ks on the name of the family.

type P0 = 'Proxy :: Proxy '()

type P1 = PS P0

type P2 = PS P1

type P3 = PS P2

type P4 = PS P3

type P5 = PS P4

type P6 = PS P5

type P7 = PS P6

type PS (p :: Proxy ks) = 'Proxy :: Proxy '(k, ks)

Coercions

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

type family Coerce (a :: k) :: l where ...

Sometimes GHC doesn't see that two type-level values are equal when they ought to be equal. Coerce lets us postpone the check to another day.

Equations

Coerce x = x

type CoerceTo l (a :: k) = Coerce a :: l

Coerce with explicit codomain.

type CoerceFrom k (a :: k) = Coerce a

Coerce with explicit domain.

type family Transp (e :: k :~: l) (x :: k) :: l where ...

Transport: coercion along an equality.

Equations

Transp (_ :: k :~: k) x = x