Should we remove the second parameter of `GenericK`?
Consider making GenericK
a single-parameter class, like Generic
, letting the methods toK
and fromK
universally quantify over the LoT
parameter instead.
The main conceptual issue with GenericK
having its current two arguments is that it is impossible to express the constraint that a given type constructor f
is generic independently of its type parameters, unless one uses QuantifiedConstraints
.
I don't mean that QuantifiedConstraints
is inherently bad, but GenericK
with only one argument would take out its necessity. Furthermore, (I hope) it would even make it easier to generalize code over arbitrary arities of type constructors.
The problems arise when deriving operations involving higher-kinded types which hide the parameters of generic type constructors, such as the following existential type:
data Ex :: (Type -> Type) -> Type where
Ex :: forall f a. f a -> Ex f
In this gist, the Ex
type allows us to define parsers for GADTs f
as functions
genericReadEx :: _ => String -> Maybe (Ex f)
so that f
's hidden type index may depend on the input:
But what constraint to give genericReadEx
? A first attempt would be forall l. GenericK f l
. However, GenericK
instances explicitly match on the l
constructor, so they are not sufficiently parametric: we actually have to write forall a. GenericK f (a :&&: LoT0)
.
-
We must use
QuantifiedConstraints
, which might be fine in itself, but does require extra expertise on top of generics. -
And we have to unfold
LoT
tuples manually.
For similar reasons, in the implementation, we also need to define a specialized variant of Ex
for generic representations, instead of reusing Ex
:
data KEx :: (LoT (k -> Type) -> Type) -> Type where
KEx :: forall f a. f (a :&&: LoT0) -> KEx f
Moreover, the code is now quite specific to type constructors of arity 1. I conjecture that a lot of the work in generalizing that to higher arities could be refactored into the kind-generics library as part of the removal of GenericK
's second argument.
For instance, as a first step in my working example (in the gist linked above), we could generalize the existential type Ex
to hide the arguments of a type constructor of arbitrary arity/kind k
:
data Ex :: k -> Type where
Ex :: forall (f :: k) (a :: LoT k). f :@@: a -> Ex f
But that requires making :@@:
"lazier" than it is currently.