和与异质和之间的一般同构

是否有 Haskell 库提供（或协助编写）总和类型与关联的异构总和类型之间的通用同构？

采用以下总和类型，

data TR = TR_Index | TR_Inner R

现在我们将它与异质和联系起来NS I xs https://hackage.haskell.org/package/sop-core-0.5.0.2/docs/Data-SOP.html#t:NS（其中“xs”由类型类定义；请参阅MotleyRouteSubRoutes以下）。然后定义一个同构来来回转换：

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 {}
      )

我的目标是写motleyRouteIso一般地（以及定义MotleyRouteSubRoutes一般而言，但这可能超出了此处的范围）。我打算从头开始使用generics-sop，但我想知道是否已经有一个图书馆可以为我做到这一点。generic-optics提供了一个IsList https://hackage.haskell.org/package/generic-optics-2.2.1.0/docs/Data-Generics-Product-HList.html但这适用于乘积而不是总和。

（有关完整上下文，请参阅this PR https://github.com/srid/ema/pull/93)

到目前为止还没有看到任何答案，我假设目前不存在这样的预构建解决方案。所以这是我基于的方法generics-sop.

RGeneric

首先我添加了一个RGenerictype-class 来缩小路由 ADT 的构造函数只能包含 0 或 1 个产品的情况：

-- | 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

这个实例的实现相当简单，使用generics-sop。你可以在这里看到它 https://github.com/srid/ema/pull/93/commits/9b9ca3712cda6051fcfa493c307838e5edc89882 (the RouteNP约束捕获了我们感兴趣的路线类型的预期“形状”）。

介绍Coercible用于举重

请注意，各个类型MotleyRouteSubRoutes或多或少可以强制路由类型构造函数。因此，我利用这些知识从方程中“消除”了特定类型，从而向通用实现迈出了一大步。具体来说：

@@ -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 {}
       )

请注意，在新版本中没有引用SingletonRoute or PrefixedRoute.

完整差异在这里 https://github.com/srid/ema/pull/93/commits/f9c7908bf8b0a622b18ea34eea41b258d55596ff.

通用ISO

有了这个地方，现在可以非常简单地通用实施motleyRouteIso using trans_NS https://hackage.haskell.org/package/sop-core-0.5.0.2/docs/Data-SOP-NS.html#v:trans_NS因为Coercible约束为我们完成了所有繁重的工作，RGeneric抽象出处理路线类型的预期“形状”。它看起来像这样：

-- 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

The 改变就在这里 https://github.com/srid/ema/pull/93/commits/e458f6228c00a9b32ac92119f4e47c673e2ef04f.