kind-generics-th
Template Haskell support for generating `GenericK` instances
Version on this page: | 0.1.0.0 |
LTS Haskell 22.37: | 0.2.3.3 |
Stackage Nightly 2023-12-26: | 0.2.3.3 |
Latest on Hackage: | 0.2.3.3 |
kind-generics-th-0.1.0.0@sha256:ed33aec0a6f80d45e9cc91e48bfa06cdb1b54b98b460338f3a622da76ecd7451,1392
Module documentation for 0.1.0.0
- Generics
- Generics.Kind
kind-generics-th
: Template Haskell support for generating GenericK
instances
This package provides Template Haskell functionality to automatically derive
GenericK
instances. Currently, this only supports the version of GenericK
as found in the kind-generics
library. (The GenericK
class found in
kind-generics-sop
is not supported at the moment.)
How to use this library
To derive instances of GenericK
for a data type, simply pass the Template
Haskell–quoted Name
of the type to the deriveGenericK
function, as in the
following example:
$(deriveGenericK ''Either)
If you wish to pass a data family instance, one can pass the name of a constructor belonging to the particular family instance, such as in the following example:
data family Foo a b
data instance Foo Int b = MkFooInt b
$(deriveGenericK 'MkFooInt)
You will likely need to enable most of these language extensions in order for GHC to accept the generated code:
DataKinds
EmptyCase
(if using an empty data type)FlexibleInstances
MultiParamTypeClasses
PolyKinds
(if using a poly-kinded data type)TemplateHaskell
TypeFamilies
How many GenericK
instances are generated
deriveGenericK
typically generates multiple GenericK
instances per data
type, as there is one GenericK
instance per partial application of a data
type constructor. For instance, $(deriveGenericK ''Either)
will generate
three GenericK
instances:
instance GenericK (Either a b) LoT0 where ...
instance GenericK (Either a) (b :&&: LoT0) where ...
instance GenericK Either (a :&&: b :&&: LoT0) where ...
Not every data type can be partially applied all the way in this fashion, however. Some notable counterexamples are:
-
Data family instances. In the following example:
data family Bar a b data instance Bar a a = MkBar a
One cannot partially apply to
Bar a a
to simplyBar a
, so$(deriveGenericK 'MkBar)
will only generate a single instance forGenericK (Bar a a) LoT0
. -
Dependent kinds.
kind-generics
is not currently capable of representing data types such as the following in their full generality:data Baz k (a :: k)
Because the
k
type variable is used in the kind ofa
(i.e., it is used in a visible, dependent fashion). As a consequence,$(deriveGenericK ''Baz)
will only generate the following instances:instance GenericK (Baz k a) LoT0
instance GenericK (Baz k) (a :&&: LoT0)
-
Data types with type family applications. In the following example:
type family Fam a newtype WrappedFam a = WrapFam (Fam a)
It is impossible to write a
GenericK
instance for a partial application ofWrappedFam
, since the representation type would necessarily need to partially applyFam
, which GHC does not permit. Therefore,$(deriveGenericK ''WrappedFam)
will only generate a single instance forGenericK (WrappedFam a) LoT0
.There are some uses of type families that are not supported altogether. For instance, if a type family is applied to an existentially quantified type variable, as in the following example:
data ExFam where MkExFam :: forall a. Fam a -> ExFam
Representing
ExFam
would fundamentally require a partial application ofFam
, astype RepK ExFam = Exists * (Field (Fam :$: Var0))
. As a result, it is impossible to giveExFam
aGenericK
instance.Note that not all type families are problematic. For instance:
type family Fam2 :: * -> * newtype WrappedFam2 a = WrapFam2 (Fam2 a)
In this example,
Fam2
is perfectly fine to partially apply, so$(deriveGenericK ''WrappedFam2)
will generate two instances (as opposed to just one, as was the case forWrappedFam
).
Limitations
kind-generics
is capable of representing a wide variety of data types. The
Template Haskell machinery in this library makes a best-effort attempt to
automate the creation of most of these instances, but there are a handful of
corner cases that it does not handle well. This section documents all of the
known limitations of deriveGenericK
:
-
Data constructors with rank-n field types (e.g.,
(forall a. a -> a)
) are currently not supported. -
Data constructors with unlifted field types (e.g.,
Int#
or(# Bool #)
) are unlikely to work. -
GADTs that make use of certain forms of kind equalities are currently not supported. For example:
data Quux (a :: k) where MkQuux :: forall (a :: *). Maybe a -> Quux a
If one were to rewrite
Quux
to make the existential quantification explicit, it would look like this:data Quux (a :: k) = forall (a' :: *). (k ~ Type, a' ~~ a) => MkQuux (Maybe a')
Therefore, we ought to get a
GenericK
instance like this:instance GenericK (Quux :: k -> *) (a :&&: LoT0) where type RepK (Quux :: k -> *) = Exists * ((Kon (k ~ Type) :&: (Var0 :~~: Var1)) :=>: Field (Maybe :$: Var0)) ...
Devising an algorithm that converts the original GADT definition of
Quux
into the explicitly existential form is not straightforward, however. In particular,deriveGenericK
only detects thek ~ *
part correctly at the moment, so it will generate an ill kinded instance forQuux
.