Generics: Documentation of `:.:` + formulate `Rec1` in terms of `:.:` and `Par1`?
I was a bit confused when I investigated the Rep1
representation of the following nested datatype:
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveFunctor #-}
module Lib where
import GHC.Generics
data Fork a = Fork a a
deriving (Generic, Functor, Generic1)
data Perfect a = Zero a | Succ (Perfect (Fork a))
deriving (Generic, Functor, Generic1)
In GHCi, I get (after stripping off metadata)
> :kind! Rep1 Perfect
Rep1 Perfect :: * -> *
= Par1 :+: (Perfect :.: Rec1 Fork)
Similarly to the definition of rose trees in https://hackage.haskell.org/package/base-4.16.0.0/docs/GHC-Generics.html#g:17, we get a :.:
due to the nesting. But what I found confusing is the lack of Rec1
around the left arg of :.:
, Perfect
. I assumed that similar to :*:
, both left and right args of :.:
would be ... well, some type constructor used in the result of Rep1
, for which we have no explicit kind (which IMO makes GHC.Generics a bit awkward to use, because you never know whether you have matched on all type constructors that can happen in a Rep1
).
But in this case, clearly the RHS of :.:
is such a type constructor of the Rep1
result kind (Rec1 Fork
), whereas the LHS Perfect
is not! It doesn't have the "pseudo-/sub-kind" of * -> *
I would have expected; it is in fact an arbitrary type of kind * -> *
.
So I read the original paper on the Generics impl and there we have
Note the arg
function. When it sees a field type such as Perfect (Fork a)
, it matches the fourth GRHS, because isRep1 Perfect
holds (because it has a Rep1
instance) and Fork a
is neither ground (it mentions the parameter a
), nor exactly the parameter a
(in which case it would match the third GRHS, as it does for Fork a
).
That suggests that indeed, the LHS of :.:
is an arbitrary type constructor of kind * -> *
which has a Generic1
instance. I wish that the documentation for :.:
mentioned this asymmetry!
And now that I think of it, why do we need Rec1
in the first place? The way I see it, Rec1 f
is literally just f :.: Par1
. We'd get
> :kind! Rep1 Perfect
Rep1 Perfect :: * -> *
= Par1 :+: (Perfect :.: (Perfect :.: Par1))
I guess :.:
is a bit more complex to think about and only relevant in the nested data type case at the moment. Nevertheless, a good design would force you to think about :.:
in generic functions from the get go. The programmer then would match on f :.: Par1
only if they really can't come up with a polymorphically recursive function that properly handles :.:
.
So I have two requests:
- Update the documentation to reflect the asymmetry of
:.:
, namely that the LHS is always a type constructor that has aGeneric1
/Rep1
instance, whereas the RHS is aRep1
generic view. - Deprecate
Rec1
in favor of(:.: Par1)
, just as we deprecatedPar0
in favor ofRec0
.
I really want (1), I don't necessarily need (2). Although (2) means that we end up with Rec0
and Par1
, which is a bit strange. Maybe we should simply name the former K
and the latter P
?