Hi! Before starting with generics support at the type level, please first improve the generics support at the value level. When I looked at it the last time, there were some apparent leftovers in the form of types or type parameters never used. In addition, it seems awkward that you have to pass these p-parameters around when working with types of kind *, and that there is no possibility to work with types with more than one parameter. I think that GHC’s approach to generics is very good in general, but that the GHC.Generics module looks a bit unpolished and ad- hoc at the moment. Maybe it would be possible to solve the abovementioned problems using TypeInType. All the best, Wolfgang Am Donnerstag, den 31.08.2017, 15:37 -0400 schrieb David Feuer:
I've been thinking for several weeks that it might be useful to offer type-level generics. That is, along with
to :: Rep a k -> a from :: a -> Rep a
perhaps we should also derive
type family To (r :: Rep a x) :: a type family From (v :: a) :: Rep a x
This would allow us to use generic programming at the type level For example, we could write a generic ordering family:
class OrdK (k :: Type) where type Compare (x :: k) (y :: k) :: Ordering type Compare (x :: k) (y :: k) = GenComp (Rep k ()) (From x) (From y)
instance OrdK Nat where type Compare x y = CmpNat x y
instance OrdK Symbol where type Compare x y = CmpSymbol x y
instance OrdK [a] -- No implementation needed!
type family GenComp k (x :: k) (y :: k) :: Ordering where GenComp (M1 i c f p) ('M1 x) ('M1 y) = GenComp (f p) x y GenComp (K1 i c p) ('K1 x) ('K1 y) = Compare x y GenComp ((x :+: y) p) ('L1 m) ('L1 n) = GenComp (x p) m n GenComp ((x :+: y) p) ('R1 m) ('R1 n) = GenComp (y p) m n GenComp ((x :+: y) p) ('L1 _) ('R1 _) = 'LT GenComp ((x :+: y) p) ('R1 _) ('L1 _) = 'GT GenComp ((x :*: y) p) (x1 ':*: y1) (x2 ':*: y2) = PComp (GenComp (x p) x1 x2) (y p) y1 y2 GenComp (U1 p) _ _ = 'EQ GenComp (V1 p) _ _ = 'EQ
type family PComp (c :: Ordering) k (x :: k) (y :: k) :: Ordering where PComp 'EQ k x y = GenComp k x y PComp x _ _ _ = x
For people who want to play around with the idea, here are the definitions of To and From for lists:
To ('M1 ('L1 ('M1 'U1))) = '[] To ('M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))) = x ': xs From '[] = 'M1 ('L1 ('M1 'U1)) From (x ': xs) = 'M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))
David _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs