Type-level generics
David Feuer
david at well-typed.com
Thu Aug 31 19:37:15 UTC 2017
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
More information about the ghc-devs
mailing list