我们能想到 Haskell 中的非对称乘积数据类型吗？

Question

Control.Category.Constrained.Cartesian 是具有一些自然变换的幺半群类别的类（乘积为(,)，单位默认为()；乘积不能更改，与Control.Category.Constrained.CoCartesian 中的总和不同）。

• regroup 和 regroup' 用于 (a, (b, c)) ≅ ((a, b), c)；
• attachUnit 和 detachUnit 用于 a ≅ (a, unit)。

他们几乎给了我们幺半群。唯一剩下的是(unit, a) ≅ a。这里我们使用(,)对称：(a, b) ≅ (b, a)。

据我所知，它不是一般属性。 Bartosz Milewski 将该属性归因于对称的幺半群类别（例如，here）。

Haskell 中是否存在一些不对称的产品类型？

Answer 1

这是一个对类型的非交换操作（可能有一个更简单的例子，但我无法想象）：

type a /\!! b = (a, ((b -> Void) -> Void))

更新：它实际上不是幺半群，因为它缺少一个（左）身份。它是关联的和不可交换的。假设它足够接近。

直觉上第二个成分是命题“Not (Not b)”，在直觉逻辑中不等价于“b”（所以(/\!!)不可交换），但等价于“Not ( Not (Not (Not b))"（所以(/\!!) 是关联的）。

这也依赖于(b -> Void) -> Void 是一个实际上无用的类型，因为所有居民在观察上都是平等的，所以我们可以用类型的同构来识别逻辑等价。

（从技术上讲，“同构”的概念是相对于居民的“平等/等价”概念而言的，为了这个例子的目的，我们选择观察平等。）

对于关联性（使用(/\) 作为(,) 的中缀表示法）

   a /\!! (b /\!! c)
=  a /\ Not (Not (b   /\ Not (Not c))
  {- distribute (Not (Not _)) over (/\)) -}
=  a /\ (Not (Not b)  /\ Not (Not (Not (Not c))))
=  a /\ (Not (Not b)  /\ Not (Not c))
  {- associativity of (/\) -}
= (a /\  Not (Not b)) /\ Not (Not c)
= (a /\!! b) /\!! c

同样值得注意的是，关于类型，存在人为的限制。受约束的类别包提出了类别具有作为对象的类型的任意要求。一般来说，一个范畴中的对象和态射可以是任何东西。

再举一个例子（实际上是一系列例子），任何幺半群都对应一个幺半群范畴，其中对象是幺半群的元素，并且只有恒等态射（它是一个discrete category）。选择任何非交换幺半群，然后将其视为具有对象上的乘积的离散类别，它是幺半群且非对称的。

---

旁注：尽管类名称为Cartesian，但它的定义和描述最接近于对称单曲面类别的传统概念，正如您所说。该文档警告不要与“笛卡尔封闭类别”混淆，但有一个更密切相关的概念 "cartesian monoidal categories"。该库中的 Cartesian 类缺少一些关键成员，这些成员被认为是其近似值，而不是对称幺半群类别的更一般概念。