haskell - 笛卡尔类的这些类扩展是做什么用的？

Question

Cartesian 来自 constrained-category 的类(class)项目用于类别，对象的产品，其中再次属于同一类别的对象。
我想知道类(class)Cartesian扩展:

class ( Category k                                      {- 1 -}
      , Monoid (UnitObject k)                           {- 2 -}
      , Object k (UnitObject k)                         {- 3 -}
      -- , PairObject k (UnitObject k) (UnitObject k)   {- 4 -}
      -- , Object k (UnitObject k,UnitObject k)         {- 5 -}
      ) => Cartesian k where
...

积分 1和 3非常简单:

1:Cartesian扩展 Category .

3:UnitObject k确实应该是 k 中的一个对象.

其他点让我感到困惑:

2:我们为什么要UnitObject k成为 Monoid ?一个适当的单位确实是一个幺半群(() <> () = () 和 mempty = () ；对于所有其他单位也是如此，因为只有一个单位模像 unitType2Id ~() = id 这样的同构)，但它是必要条件，而不是充分条件。我们为什么不实现一些类，例如:

class ProperUnit u where
    toUnitType :: u -> ()
    fromUnitType :: () -> u

符合以下法律:fromUnitType . toUnitType = id .
我认为两者都不扩展Monoid ，也不是 ProperUnit类来为代码添加额外的功能，只是让它更惯用。还是我错了？

4:这个被注释掉了。为什么这样？我们首先需要这对两个单元做什么？不是和普通单位一样好吗？它们显然是同构的。

5:这个又被注释掉了。为什么这样？为什么我们需要这样一对作为类别中的对象？这个条件不是比上一个弱吗？ 1 PairObject type 对pairs 有额外的限制。如果这样的一对实际上是类别中的一个对象，它仍然不一定满足PairObject。限制，在这种情况下我们根本不能使用它。

谁能解释一下这三点背后的逻辑。

1 正如 Bartosz Milewski 指出的那样， PairObject (目前更名为 PairObjects )和 ObjectPair 是不同的限制，后者更严格，保证我们在一个类别中构成一对实际的“可张量”对象，其中这样的一对作为对象存在。其实点 1 , 3 , 4和 5相当于 ObjectPair k (UnitObject k) (UnitObject k) .尽管如此，我还是不太明白为什么我们会接受这样的条件(将其注释掉)。

Answer 1

就像 Bartosz Milewski 评论的那样:严格来说，这些都不应该是必要的。在数学上，您只需定义您的类别和单位的对象是什么，所有张量积也是如此，((),a) ≡ a等等，以及 PairObject是多余的。
问题是......好吧，实用主义和Haskell。就像，众所周知，((a,b),c) 之间的适当相等和 (a,(b,c))就在窗外。但同样从实际开发的角度来看，您不一定想以这种演绎数学的方式进行思考。我发现保留 Category 更实用。类简单，然后向更专业的类添加一些特别的约束，而不是从一开始就要求所有东西都尽可能地在数学上保持。 (当在 Object 中实现这些约束时，我发现自己不得不在 GADT 字段中携带更多类型信息并再次显式解包元组，PairObject 通常可以在没有尴尬的值级模式匹配的情况下取代。)
具体来说，一些 Type->Type->Type s 可以很容易地成为 Category 的一个实例, 实现 id ，但需要更复杂的机械，例如*** .在这种情况下，严格来说，您使用的是两个不同的类别:Category 描述的一个类别。例如，它的一个较小的子类别是笛卡尔幺半群。甚至是一整套类别，每个类别都有不同的PairObject -连接的对象类。
至于为什么Monoid :正如您所猜想的那样，它并不是真正适合该任务的类(class)，但它确实可以完成工作并且很普遍。您的 ProperUnit类不会给你更多的工具，因为 toUnitType方法总是微不足道的，fromUnitType ≡ const mempty .我相信你在这里真正想到的是

class Monoid a => Singleton a where
  hasOnlyUnit :: a -> {Proof that a==mempty}

但如果没有依赖类型，这很尴尬。我也不确定它是否真的会给我们带来任何东西。
不幸的是这个名字 Monoid在这种情况下，它有点像红鲱鱼。
具体来说，它解决的“工作”与全局元素有关，尤其是在使用 Agent 时。用于将分类组合链编码为 lambda 表达式的类型——所有这些都继承了 Conal Elliot 在硬件编译等方面的工作，但作为一个 Haskell 库。
我反复琢磨了几次放置各种约束的最佳位置，注释掉的 PairObject k (UnitObject k) (UnitObject k)约束是其中的一个产物:这些约束在道德上应该成立，但我发现在定义实例时明确要求它们会导致更多问题，而不是在使用它们时解决的问题。