Void 是初始元素还是零元素？

Question

ZeroObject的Control.Category.Constrained默认Void。很明显，这Void是一个初始对象：

{-# LANGUAGE EmptyCase #-}

absurd :: Void -> a
absurd x = case x of

但是为什么叫它ZeroObject呢？一方面，由于UnitObject默认为()并且我们与算术非常匹配：

((), x) ? x ? (x, ()); 1 * x = x = x * 1.
Void + x ? x ? x + Void; 0 + x = x = x + 0.

但另一方面，术语零对象用于同时为initial和terminal 的对象。说实话，我看不出Void是终端。与absurd帮助我们运行声称属于Void类型的错误不同，我认为a -> Void不要做任何有用的事情，因为不能保证参数保持错误，因此每次都会抛出相同的异常。 _{请参阅 HTNW 的评论。}

我Void不是终端对象是对的吗？我们使用Void的终端功能还是ZeroObject选择匹配算术的名称？

Answer 1

虽然“零对象”确实有时用于既是初始又是终结的对象，但在宏大的数学传统中，它有时也以不同且相互矛盾的方式使用！

具体来说，在谈论副产品时，使用符号 0 来指代初始对象（这就是副产品的身份）是很常见的。例如，参见关于联积的维基百科页面（在“所有有限联积”的讨论中，“0 表示初始对象”）。这就是此处使用“ZeroObject”的意义：初始，更重要的是，副产品的身份。

（顺便说一下，由于与算术的类比，范畴论者有可能选择符号 0 作为联积的恒等式；但是这个库使用术语 ZeroObject 的原因是因为 CT 使用 0 表示恒等式，而不是因为算术确实如此。换句话说，CT 因为算术而使用 this 的事实是远离原因的间接一步。）