Type-level generics
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
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
Seems that by making a class you can "prove" by requiring this isomorphism: class (To r ~ v, From v ~ r) -- , To (From v :: Rep a x) ~ v) => TypeGeneric a (r :: Rep a x) (v :: a) where type To r :: a type From v :: Rep a x See attachment or [1] for the whole file. Cheers, Oleg [1]: https://gist.github.com/phadej/fab7c627efbca5cba16ba258c8f10337 On 31.08.2017 23:22, David Feuer wrote:
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
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
On Fri, Sep 1, 2017 at 2:23 PM, Wolfgang Jeltsch
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
I was just about to complain about this myself, since every year or so I go fail to figure out GHC.Generics after tripping over lots of out of date documentation, confusing type aliases, and obsolete aliases, and wrong examples, but I just looked again and it seems like GHC.Generics got a major update in ghc 8. It looks like there's still one confusing reference to Par0: "Note how Par0 and Rec0 both being mapped to K1 allows us to define a uniform instance here. " but at least it's not tangled up in the already very confusing examples and signatures. I think that sentence can be deleted entirely now? I have no idea what it's trying to express. So thanks to whoever did that. I'll give it another try.
participants (4)
-
David Feuer -
Evan Laforge -
Oleg Grenrus -
Wolfgang Jeltsch