Family of families: featherweight defunctionalization

Motivation

This package transforms regular type families into "first-class families". It does so without declaring dummy data types as defunctionalization symbols, avoiding namespace pollution.

Featherweight defunctionalization

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.

GHC.TypeNats.+
-- 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, only an Eval instance for its name.
• Decentralization: Every type family induces a unique Eval instance, 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 Fcf.Family.

Usage

Promote a type family

To promote a type family, the necessary boilerplate can be generated with Template Haskell, using the function Fcf.Family.TH.fcfify.

fcfify ''MyTypeFamily

-- Examples
fcfify ''(GHC.TypeNats.+)
fcfify ''Data.Type.Bool.If

This generates instances of Eval and auxiliary type families for that former instance to be well-defined.

Use the promoted type family

This allows using the defunctionalization symbol Family indexed by the type family's name---a tuple of strings constructed with MkName.

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

  Eval (Family (MkName "base" "GHC.Type.Bool" "If") P1 '( 'True, '("yes", '("no", '()))))
= If 'True "yes" "no"
= "yes"

The familyName function converts the name of an actual family to an fcf-family name in Template Haskell.

  Eval (Family $(familyName ''+) P0 '(1, '(2, '())))
= 3

  Eval (Family $(familyName ''If) P1 '( 'True, '("yes", '("no", '()))))
= "yes"

Existing instances

• The library fcf-base contains instances for type families defined in base.
• The module Fcf.Family.Meta contains the instance for Eval.

Limitations

• 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 Type. Lifting this restriction requires either access to more typing information from the compiler via TH, or some implementation of kind inference in TH.