One other thing I should add. We'd really, really like to have isomorphism evidence:
toThenFrom :: pr p -> To (From x :: Rep a p) :~: (x :: a) fromThenTo :: pr1 a -> pr2 (r :: Rep a p) -> From (To r :: a) :~: (r :: Rep a p) I believe these would make the To and From families considerably more useful. Unfortunately, while I'm pretty sure those are completely legit for any Generic-derived types, I don't think there's ever any way to prove them in Haskell! Ugh. On Thursday, August 31, 2017 3:37:15 PM EDT David Feuer wrote: > 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