笛卡尔类的那些类扩展是什么？

问题描述

Cartesian 项目中的 constrained-category 类用于类别，对象的产品再次属于同一类别的对象。

我想知道 Cartesian extends 的类：

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：这个又被注释掉了。为什么这样？为什么我们需要这样一对才能成为类别中的对象？这个条件不是比前一个弱吗？¹PairObject 类型对对设置了额外的限制。如果这样的一对实际上是类别中的对象，它仍然不一定满足 PairObject 限制，在这种情况下我们根本无法使用它。

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

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

解决方法

就像 Bartosz Milewski 评论的那样：严格来说，这一切都没有必要。在数学上，您只需定义一下您的类别和单位的对象是什么，所有张量积也是如此，((),a) ≡ a 等，而 PairObject 是多余的。

问题是……嗯，实用主义和 Haskell。就像，众所周知，((a,b),c) 和 (a,(b,c)) 之间的适当相等就在窗外。但同样从实际开发的角度来看，您不一定想以这种演绎数学的方式思考。我发现让 Category 类保持简单，然后向更专业的类添加一些临时约束更实用，而不是从一开始就要求所有内容都尽可能在数学上保持不变。（当在 Object 中实现这些约束时，我发现自己必须在 GADT 字段中携带更多类型信息并再次显式解包元组，PairObject 通常可以取代它而不会出现尴尬的值级模式匹配。 )

特别是，一些 Type->Type->Type 可以很容易地成为 Category 的实例，只需一个光照约束来实现 id，但需要更复杂的机制，例如***。在这种情况下，严格来说，您使用的是两个不同的类别：由 Category 实例描述的类别，以及它的一个较小的子类别，即笛卡尔幺半群。或者甚至是整个类别系列，每个类别都有不同的 PairObject 连接对象类。

至于为什么 Monoid：正如您已经猜到的那样，它确实不是适合该任务的类，但它可以完成工作并且很普遍。您的 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) 约束是其产物：这些约束在道德上应该成立，但我发现的是明确的在定义实例时要求它们比在使用它们时解决的问题更多。

category-theory haskell haskell monoids