Is there a Haskell library providing (or assisting in writing) generic isomorphism between a sum type and an associated heterogenous sum type?
Take the following sum type,
data TR = TR_Index | TR_Inner R
Now we associate it with a heterogenous sum NS I xs
(where the 'xs' is defined by a type-class; see MotleyRouteSubRoutes
below). And then define a isomorphism to convert back and forth:
instance MotleyRoute TR where
-- `SingletonRoute s` is isomorphic to `()`
-- `PrefixedRoute s r` is isomorphic to `Const r s`
type MotleyRouteSubRoutes TR =
'[ SingletonRoute "index.html"
, PrefixedRoute "inner" R
]
motleyRouteIso =
iso
( \case
TR_Index -> Z $ I SingletonRoute
TR_Inner r -> S $ Z $ I $ PrefixedRoute r
)
( \case
Z (I SingletonRoute) -> TR_Index
S (Z (I (PrefixedRoute r))) -> TR_Inner r
S (S x) -> case x of {}
)
My goal here is to write motleyRouteIso
generically (as well as define MotleyRouteSubRoutes
generically, but that maybe outside the scope here). I was going to do it from scratch using generics-sop
, but I wonder if there already is a library that does this for me. generic-optics
provides a IsList
but that works for products not sums.
(For full context, see this PR)
CodePudding user response:
Having seen no answer on this so far I'll assume for the moment no such prebuilt solution exists. So here's an approach I went with based on generics-sop
.
RGeneric
First I added a RGeneric
type-class to narrow the case where a route ADT can have constructors with 0 or 1 product only:
-- | Like `Generic` but for Route types only.
class RGeneric r where
type RCode r :: [Type]
rfrom :: r -> NS I (RCode r)
rto :: NS I (RCode r) -> r
The implementation of this instance is fairly straightforward using generics-sop
. You can see it here (the RouteNP
constraint captures the expected "shape" of route types we are interested in).
Introduce Coercible
for heavy-lifting
Note that the individual types in MotleyRouteSubRoutes
are more or less coercible to the route type constructors. So I used that knowledge to "eliminate" the specific types from the equation thus getting one large step closer to a generic implementation. Specifically:
@@ -95,12 95,12 @@ instance MotleyRoute TR where
motleyRouteIso =
iso
( \case
- TR_Index -> Z $ I SingletonRoute
- TR_Inner r -> S $ Z $ I $ PrefixedRoute r
TR_Index -> Z $ coerce ()
TR_Inner r -> S $ Z $ coerce r
)
( \case
- Z (I SingletonRoute) -> TR_Index
- S (Z (I (PrefixedRoute r))) -> TR_Inner r
Z (I (coerce -> ())) -> TR_Index
S (Z r) -> TR_Inner $ coerce r
S (S x) -> case x of {}
)
Notice how in the new version there is no reference to SingletonRoute
or PrefixedRoute
.
Generic Iso
With this place, it is now pretty straightforward to generically implement motleyRouteIso
using trans_NS
because the Coercible
constraint does all the heavy lifting for us, with RGeneric
abstracting out dealing with expected 'shape' of the route type. It looks like this:
-- Rough code (leaving out the constraints)
gmotleyRouteIso =
iso (gtoMotley @r . rfrom) (rto . gfromMotley @r)
where
gtoMotley = trans_NS (Proxy @Coercible) coerce
gfromMotley = trans_NS (Proxy @Coercible) coerce