What are those class extensions for the Cartesian class for?

Question

The Cartesian class from the constrained-category project is for categories, products of objects in which are objects in the same category yet again.

I wonder about the classes 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
...

Points 1 and 3 are pretty straightforward:

• 1: Cartesian extends Category.
• 3: The UnitObject k shall indeed be an object in k.

Other points confuse me:

• 2: Why do we want UnitObject k to be a Monoid? A proper unit is indeed a monoid (() <> () = () and mempty = (); the same goes for all other units as there exists only one unit modula the isomorphisms like unitType2Id ~() = id), but it is a necessary condition, not a sufficient one. Why don't we implement some class like:

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

  With the following law: fromUnitType . toUnitType = id. I reckon extending neither Monoid, nor the ProperUnit classes to add extra features to the code, simply making it more idiomatic. Or am I wrong?

• 4: This one is commented out. Why so? What did we need the pair of two units for in the first place? Isn't it as good as a regular unit? They are clearly isomorphic.

• 5: This one is commented out once again. Why so? And why did we need such a pair to be an object in the category? Isn't this condition weaker than the previous one?¹ The PairObject type institutes extra restrictions concerning pairs. If such a pair is, in fact, an object in the category, it still doesn't necessarily satisfy the PairObject restriction, in which case we can't use it at all.

Can someone, please explain the logic behind these 3 points.

---

¹ As Bartosz Milewski pointed out, PairObject (currently renamed into PairObjects) and ObjectPair are different restrictions, the latter being more strict, guaranteeing that we make up pairs of actual "tensorable" objects in a category, where such a pair exists as an object. In fact, points 1, 3, 4 and 5 are equivalent to ObjectPair k (UnitObject k) (UnitObject k). Still, I do not quite understand why we entertain such a condition (leaving it commented out).

Answer 1

就像 Bartosz Milewski 评论的那样：严格来说，这一切都没有必要。从数学上讲，您只需定义一次类别和单位的对象，并且所有张量积也是如此，等等((),a) \xe2\x89\xa1 a，并且PairObject是多余的。

\n

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

\n

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

\n

至于为什么Monoid：正如您所猜测的，它并不是真正适合该任务的类，但它可以完成工作并且很普遍。您的ProperUnit类不会为您提供任何更多工具，因为该toUnitType方法总是微不足道的并且fromUnitType \xe2\x89\xa1 const mempty. 我相信你真正想到的是

\n

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

\n

但如果没有依赖类型，这就很尴尬。我也不确定它是否真的会给我们带来任何东西。

\n

不幸的是，这个名字Monoid在这种情况下有点转移注意力。

\n

具体来说，它解决的 \xe2\x80\x9cjob\xe2\x80\x9d 与全局元素有关，特别是当使用Agent将分类组合链编码为 lambda 表达式的类型时 \xe2\x80\x93 所有这些都在脚步中Conal Elliot 在硬件编译等方面的工作，但作为 Haskell 库。

\n

我几次反复思考放置各种约束的最佳位置，注释掉的PairObject k (UnitObject k) (UnitObject k)约束是这样的产物：这些约束在道德上应该成立，但我发现明确要求它们会导致更多定义实例时遇到的问题比使用实例时解决的问题要多。

\n