Type-level generics

Ryan Scott ryan.gl.scott at gmail.com
Fri Sep 1 13:12:26 UTC 2017

While we're on the topic, I'll mention that at one point I attempted
to modify the singletons [1] library so that it would automatically
generate promoted (i.e., type-level) and singled versions of Generic
instances for any data type that derived Generic. I wasn't successful,
since it turns out singletons are difficult to adapt to data types
with higher-kinded types [2] and type classes with associated type
families [3], but I did manage to write some examples on a very
limited subset of GHC.Generics in this gist [4].

The promoted version of Generic (PGeneric) in that gist works pretty
much identically to Oleg's version, but with one notable difference: I
don't attempt to put the Generic laws as a superclass of PGeneric.
Instead, I make the laws class methods of the singled version of
Generic (SGeneric). I found it more convenient to do it this way since
I needed to pattern-match on these proofs directly in a generic
implementation of decidable equality, but I'm sure this isn't the only
way it could be done.

Speaking of which, it astounds me that the Generic laws aren't
documented in the Haddocks! We really should do that.

Ryan S.
[1] http://hackage.haskell.org/package/singletons
[2] See the extended discussion in
[3] https://github.com/goldfirere/singletons/issues/198
[4] https://gist.github.com/RyanGlScott/daeb63be7885244d9882dcbb1bbc10cc

More information about the ghc-devs mailing list