CODEWITHSUNDEEP
haskelltypescategory-theory
Zhiltsoff Igor
Zhiltsoff Igor

Reputation: 1822

Is Void an initial or zero element?

ZeroObject of Control.Category.Constrained defaults to Void. It is obvious that Void is an initial object:

{-# LANGUAGE EmptyCase #-}

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

But why is it called ZeroObject? On one hand, since UnitObject defaults to () and we have a very nice match with arithmetic:

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

But on the other hand, the term zero object is used for objects that are both initial and terminal. Truth be told, I can't see how Void is terminal. Unlike absurd which helps us run the error which claims to be of Void type, I reckon a -> Void not to do anything useful as the argument is not guaranteed to hold an error, therefore making us throw the same exception every time. See HTNW's comment.

Am I right about Void not being a terminal object? Do we use Void's terminal feature or was the name ZeroObject chosen to match arithmetic?

Upvotes: 1

Views: 249

Answers (1)

Daniel Wagner
Daniel Wagner

Reputation: 153102

Although "zero object" is, indeed, sometimes used for objects that are both initial and terminal, it is also the case, in grand mathematical tradition, that it is sometimes used in a different and conflicting way!

Specifically, when talking about coproducts, it is very common to use the notation 0 to refer to an initial object (which is then the identity for the coproduct). See for example the Wikipedia page on coproducts ("0 denotes the initial object" in the discussion of "all finite coproducts"). This is the sense in which "ZeroObject" is being used here: initial, and more importantly, the identity for the coproduct.

(By the way, it is possible that category theoreticians chose the notation 0 as the identity for coproducts because of the analogy to arithmetic; but the reason this library uses the term ZeroObject is because CT uses 0 for identity, not because arithmetic does. The fact that CT uses this because of arithmetic is one step of indirection away from the reason, in other words.)

Upvotes: 6

Related Questions