Type-level generics

[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
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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs