Family of families: featherweight defunctionalization
This package transforms regular type families into
It does so without declaring dummy data types as defunctionalization symbols,
avoiding namespace pollution.
The idea is to use strings. There is an unambiguous way to refer to an existing type family:
by its fully qualified name---a triple of a package name, module name, and base name.
-- as a Name --
MkName "base" "GHC.TypeNats" "+"
All type families can be promoted to first-class using a single symbol indexed by
qualified names. That is the
Family of type families.
- No namespace pollution: Promoting a type family requires no new data type,
Eval instance for its name.
- Decentralization: Every type family induces a unique
and multiple packages may declare the same instance without conflicts.
type instance Eval (Family_ (MkName "base" "GHC.TypeNats" "+") _ '(x, '(y, '()))) = x + y
For more details on this encoding, see the module
To promote a type family, the necessary boilerplate
can be generated with Template Haskell, using the function
This generates instances of
Eval and auxiliary type families for that former
instance to be well-defined.
This allows using the defunctionalization symbol
Family indexed by the
type family's name---a tuple of strings constructed with
Eval (Family (MkName "base" "GHC.TypeNats" "+") P0 '(1, '(2, '())))
= 1 + 2
Eval (Family (MkName "base" "GHC.Type.Bool" "If") P1 '( 'True, '("yes", '("no", '()))))
= If 'True "yes" "no"
familyName function converts the name of an actual family to an fcf-family name in Template Haskell.
Eval (Family $(familyName ''+) P0 '(1, '(2, '())))
Eval (Family $(familyName ''If) P1 '( 'True, '("yes", '("no", '()))))
- The library
fcf-base contains instances for type families defined in base.
- The module
Fcf.Family.Meta contains the instance for
- There is partial support for dependently typed type families.
The kind of the result may depend on its arguments.
This package does not yet support type families where the kind of arguments
depends on other visible arguments.
- Invisible arguments are currently all assumed to be of kind
Lifting this restriction requires either access to more typing information
from the compiler via TH, or some implementation of kind inference in TH.