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

Question

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

采用以下总和类型，

data TR = TR_Index | TR_Inner R

现在我们将它与异质总和相关联NS I xs（其中“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但适用于乘积而不是求和。

（有关完整上下文，请参阅此 PR）

Answer 1

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

RGeneric

首先，我添加了一个RGeneric类型类来缩小路由 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。您可以在这里看到它（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或PrefixedRoute。

完整的差异在这里。

通用ISO

motleyRouteIso有了这个地方，现在一般实现使用就变得非常简单，trans_NS因为Coercible约束为我们完成了所有繁重的工作，RGeneric抽象出处理路线类型的预期“形状”。它看起来像这样：

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

对此的改变就在这里。