kind-generics: generic programming for arbitrary kinds and GADTs

Data type-generic programming in Haskell is restricted to types of kind * (by using Generic) or * -> * (by using Generic1). This works fine for implementing generic equality or generic printing, notions which are applied to types of kind *. But what about having a generic Bifunctor or Contravariant? We need to extend our language for describing data types to other kinds -- hopefully without having to introduce Generic2, Generic3, and so on.

The language for describing data types in GHC.Generics is also quite restricted. In particular, it can only describe algebraic data types, not the full extent of GADTs. It turns out that both problems are related: if you want to describe a constructor of the form forall a. blah, then blah must be a data type which takes one additional type variable. As a result, we need to enlarge and shrink the kind at will.

This library, kind-generics, provides a new type class GenericK and a set of additional functors F (from field), C (from constraint), and E (from existential) which extend the language of GHC.Generics. We have put a lot of effort in coming with a simple programming experience, even though the implementation is full of type trickery.

Short summary for simple data types

GHC has built-in support for data type-generic programming via its GHC.Generics module. In order to use those facilities, your data type must implement the Generic type class. Fortunately, GHC can automatically derive such instances for algebraic data types. For example:

{-# language DeriveGeneric #-}  -- this should be at the top of the file

data Tree a = Branch (Tree a) (Tree a) | Leaf a
            deriving Generic    -- this is the magical line

From this Generic instance, kind-generics can derive another one for its very own GenericK. It needs one additional piece of information, though: the description of the data type in the enlarged language of descriptions. The reason for this is that Generic does not distinguish whether the type of a field mentions one of the type variables (a in this case) or not. But GenericK requires so.

Let us look at the GenericK instance for Tree:

instance GenericK Tree (a :&&: LoT0) where
  type RepK Tree = (F (Tree :$: V0) :*: F (Tree :$: V0)) :+: (F V0)

In this case we have two constructors, separated by (:+:). The first constructor has two fields, tied together by (:*:). In the description of each field is where the difference with GHC.Generics enters the game: you need to describe each piece which makes us the type. In this case Tree :$: V0 says that the type constructor Tree is applied to the first type variable. Type variables, in turn, are represented by zero-indexed V0, V1, and so on.

The other piece of information we need to give GenericK is how to separate the type constructor from its arguments. The first line of the instance always takes the name of the type, and then a list of types representing each of the arguments. In this case there is only one argument, and thus the list has only one element. In order to get better type inference you might also add the following declaration:

instance Split (Tree a) Tree (a :&&: LoT0)

You can finally use the functionality from kind-generics and derive some type classes automatically:

import Generics.Kind.Derive.Eq
import Generics.Kind.Derive.Functor

instance Eq a => Eq (Tree a) where
  (==) = geq'
instance Functor Tree where
  fmap = fmapDefault

Type variables in a list: LoT and (:@@:)

Let us have a closer look at the definition of the GenericK type class. If you have been using other data type-generic programming libraries you might recognize RepK as the generalized version of Rep, which ties a data type with its description, and the pair of functions fromK and toK to go back and forth the original values and their generic counterparts.

class GenericK (f :: k) (x :: LoT k) where
  type RepK f :: LoT k -> *
  fromK :: f :@@: x -> RepK f x
  toK   :: RepK f x -> f :@@: x

But what are those LoT and (:@@:) which appear there? That is indeed the secret sauce which makes the whole kind-generics library work. The name LoT comes from list of types. It is a type-level version of a regular list, where the (:) constructor is replaced by (:&&:) and the empty list is represented by LoT0. For example:

Int :&&: [Bool] :&&: LoT0  -- a list with two basic types
Int :&&: [] :&&: LoT0      -- type constructor may also appear

What can you do with such a list of types? You can pass them as type arguments to a type constructor. This is the role of (:@@:) (which you can pronounce of, or application). For example:

Either :@@: (Int :&&: Bool :&&: LoT0) = Either Int Bool
Free   :@@: ([]  :&&: Int  :&&: LoT0) = Free [] Int
Int    :@@:                     LoT0 = Int

Wait, you cannot apply any list of types to any constructor! Something like Maybe [] is rejected by the compiler, and so should we reject Maybe ([] :&&: LoT0). To prevent such problems, the list of types is decorated with the kinds of all the types inside of it. Going back to the previous examples:

Int :&&: [Bool] :&&: LoT0  ::  LoT (* -> * -> *)
Int :&&: [] :&&: LoT0      ::  LoT (* -> (* -> *) -> *)

The application operator (:@@:) only allows us to apply a list of types of kind k to types constructors of the same kind. The shared variable in the head of the type class enforces this invariant also in our generic descriptions.

Helper classes: GenericS, GenericF, GenericN

If you want to turn a value into its generic representation, the fromK method of the GenericK class should be enough. Alas, that is a hard nut to crack for GHC's inference engine. Imagine you call fromK (Left True): should it break the type Either Bool a into Either :@@: (Bool :&&: a :&&: LoT0), or maybe into Either Bool :@@: (a :&&: LoT0)? In principle, it is possible that even both instances exist, although it does not make sense in the context of this library.

It turns out that the interface provided by GenericK is very helpful for those writing conversion from and to generic representations, but not so much for those using fromK and toK. For that reason, kind-generics provides three different extensions to GenericK depending on how much of the type you know:

• When the type is completely known and you have an instance for Split (which describes how to separate a type into its head and its type arguments), you should use GenericS. This is the most common scenario: for example, fromS (Left True) works as you may expect, using the GenericK instance for Either. This option also provides the closest experience to GHC.Generics.
• When you know the f in the f :@@: x, it is possible to use GenericF. In that case, you have to provide the head of the type using a type application. For example, fromF @Either (Just True).
• A third option is to indicate how many arguments should go in the list of types x to generate f :@@: x. In the previous case, you might have also used fromN @(S (S Z)) (Just True). Note that the length of the list of types is expressed as a unary number.

Describing fields: the functor F

As mentioned in the introduction, kind-generics features a more expressive language to describe the types of the fields of data types. We call the description of a specific type an atom. The language of atoms reproduces the ways in which you can build a type in Haskell:

1. You can have a constant type t, which is represented by Kon t.
2. You can mention a variable, which is represented by V0, V1, and so on. For those interested in the internals, there is a general Var v where v is a type-level number. The library provides the synonyms for ergonomic reasons.
3. You can take two types f and x and apply one to the other, f :@: x.

For example, suppose the a is the name of the first type variable and b the name of the second. Here are the corresponding atoms:

a            ->  V0
Maybe a      ->  Kon Maybe :@: V0
Either b a   ->  Kon Either :@: V1 :@: V0
b (Maybe a)  ->  V1 :@: (Kon Maybe :@: V0)

Since the Kon f :@: x pattern is very common, kind-generics also allows you to write it as simply f :$: x. The names (:$:) and (:@:) are supposed to resemble (<$>) and (<*>) from the Applicative type class.

The kind of an atom is described by two pieces of information, Atom d k. The first argument d specifies the amounf of variables that it uses. The second argument k tells you the kind of the type you obtain if you replace the variable markers V0, V1, ... by actual types. For example:

V0                     ->  Atom (k -> ks)             k
V1 :@: (Maybe :$: V0)  ->  Atom (* -> (* -> *) -> ks) (*)

In the first example, if you tell me the value of the variable a regardless of the kind k, the library can build a type of kind k. In the second example, the usage requires the first variable to be a ground type, and the second one to be a one-parameter type constructor. If you give those types, the library can build a type of kind *.

This operation we have just described is embodied by the Ty type family. A call looks like Ty atom lot, where atom is an atom and lot a list of types which matches the requirements of the atom. We say that Ty interprets the atom. Going back to the previous examples:

Ty V0                    Int                      =  Int
Ty V1 :@: (Maybe :$: V0) (Bool :&&: [] :&&: LoT0) =  [Maybe Bool]

This bridge is used in the first of the pattern functors that kind-generics add to those from GHC.Generics. The pattern functor F is used to represent fields in a constructor, where the type is represented by an atom. Compare its definition with the K1 type from GHC.Generics:

newtype F  (t :: Atom d (*)) (x :: LoT d) = F { unF :: Ty t x }
newtype K1 i (t ::  *) = K1 { unK1 :: t }

At the term level there is almost no difference in the usage, except for the fact that fields are wrapped in the F constructor instead of K1.

instance GenericK Tree (a :&&: LoT0) where
  type RepK Tree = (F (Tree :$: V0) :*: F (Tree :$: V0)) :+: (F V0)

  fromK (Branch l r) = L1 (F l :*: F r)
  fromK (Node   x)   = R1 (F x)

On the other hand, separating the atom from the list of types gives us the ability to interpret the same atom with different list of types. This is paramount to classes like Functor, in which the same type constructor is applied to different type variables.

Functors for GADTS: (:=>:) and E

Generalised Algebraic Data Types, GADTs for short, extend the capabilities of Haskell data types. Once the extension is enabled, constructor gain the ability to constrain the set of allowed types, and to introduce existential types. Here is an extension of the previously-defined Tree type to include an annotation in every leaf, each of them with possibly a different type, and also require Show for the as:

data WeirdTree a where
  WeirdBranch :: WeirdTree a -> WeirdTree a -> WeirdTree a 
  WeirdLeaf   :: Show a => t -> a -> WeirdTree a

The family of pattern functors U1, F, (:+:), and (:*:) is not enough. Let us see what other things we use in the representation of WeirdTree:

instance GenericK WeirdTree (a :&&: LoT0) where
  type RepK WeirdTree
    = F (WeirdTree :$: V0) :*: F (WeirdTree :$: V0)
      :+: E ((Show :$: V1) :=>: (F V0 :*: F V1))

Here the (:=>:) pattern functor plays the role of => in the definition of the data type. It reuses the same notion of atoms from F, but requiring those atoms to give back a constraint instead of a ground type.

But wait a minute! You have just told me that the first type variable is represented by V0, and in the representation above Show a is transformed into Show :$: V1, what is going on? This change stems from E, which represents existential quantification. Whenever you go inside an E, you gain a new type variable in your list of types. This new variable is put at the front of the list of types, shifting all the other one position. In the example above, inside the E the atom V0 points to t, and V1 points to a. This approach implies that inside nested existentials the innermost variable corresponds to head of the list of types V0.

Unfortunately, at this point you need to write your own conversion functions if you use any of these extended features (pull requests implementing it in Template Haskell are more than welcome).

instance GenericK WeirdTree (a :&&: LoT0) where
  type RepK WeirdTree = ...

  fromK (WeirdBranch l r) = L1 $         F l :*: F r
  fromK (WeirdLeaf   a x) = R1 $ E $ C $ F a :*: F x

  toK ...

If you have ever done this work in GHC.Generics, there is not a big step. You just need to apply the E and C constructor every time there is an existential or constraint, respectively. However, since the additional information required by those types is implicitly added by the compiler, you do not need to write anything else.

Implementing a generic operation with kind-generics

The last stop in our journey through kind-generics is being able to implement a generic operation. At this point we assume that the reader is comfortable with the definition of generic operations using GHC.Generics, so only the differences with that style are pointed out.

Take an operation like Show. Using GHC.Generics style, you create a type class whose instances are the corresponding pattern functors:

class GShow (f :: * -> *) where
  gshow :: f x -> String

instance GShow U1 ...
instance Show t => GShow (K1 i t) ...
instance (GShow f, GShow g) => GShow (f :+: g) ...
instance (GShow f, GShow g) => GShow (f :*: g) ...

When using kind-generics, the type class needs to feature the separation between the head and its type arguments, in a similar way to GenericK. In this case, that means extending the class with a new parameter, and reworking the basic cases to include that argument.

class GShow (f :: LoT k -> *) (x :: LoT k) where
  gshow :: f :@@: x -> String

instance GShow U1 x ...
instance (GShow f x, GShow g x) => GShow (f :+: g) x ...
instance (GShow f x, GShow g x) => GShow (f :*: g) x ...

Now we have the three new constructors. Let us start with F atom: when is it Showable? Whenever the interpretation of the atom, with the given list of types, satisfies the Show constraint. We can use the type family Ty to express this fact:

instance (Show (Ty a x)) => GShow (F a) x where
  gshow (F x) = show x

In the case of existential constraints we do not need to enforce any additional constraints. However, we need to extend our list of types with a new one for the existential. We can do that using the QuantifiedConstraints extension introduced in GHC 8.6:

{-# language QuantifiedConstraints #-}

instance (forall t. Show f (t :&&: x)) => GShow (E f) x where
  gshow (E x) = gshow x

The most interesting case is the one for constraints. If we have a constraint in a constructor, we know that by pattern matching on it we can use the constraint. In other words, we are allowed to assume that the constraint at the left-hand side of (:=>:) holds when trying to decide whether GShow does. This is again allowed by the QuantifiedConstraints extension:

{-# language QuantifiedConstraints #-}

instance (Ty c x => GShow f x) => GShow (c :=>: f) x where
  gshow (C x) = gshow x

Note that sometimes we cannot implement a generic operation for every GADT. One example is generic equality (which you can find in the module Generics.Kind.Derive.Eq): when faced with two values of a constructor with an existential, we cannot move forward, since we have no way of knowing if the types enclosed by each value are the same or not.

Conclusion and limitations

The kind-generics library extends the support for data type-generic programming from GHC.Generics to account for kinds different from * and * -> * and for GADTs. We have tried to reuse as much information as possible from what the compiler already gives us for free, in particular you can obtain a GenericK instance if you already have a Generic one.

Although we can now express a larger amount of types and operations, not all Haskell data types are expressible in this language. In particular, we cannot have dependent kinds, like in the following data type:

data Proxy k (d :: k) = Proxy

because the kind of the second argument d refers to the first argument k.