Type-level generics

[David Feuer]

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