What are those class extensions for the Cartesian class for?

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).

Like Bartosz Milewski commented: strictly speaking none of this should be necessary. Mathematically, you'd just once define what are the objects of your category and the unit, and that all tensor products are too, and ((),a) ≡ a etc., and PairObject is superfluous.

The problem is... well, pragmatism and Haskell. Like, it's well known that a proper equality between ((a,b),c) and (a,(b,c)) is right out of the window. But also from a practical development perspective you don't necessarily want to think in this deductive mathematical way. I found it to be more practical to keep the Category class simple and then add some ad-hoc constraints to the more specialised classes, rather than demanding everything to hold as mathematically as possible right from the start. (When implementing these constraints right in Object, I found myself having to carry around more type information in GADT fields and explicitly unpacking tuples again, which the PairObject can often supplant without awkward value-level pattern matching.)

Specifically, some Type->Type->Types can easily be made an instance of Category, with only a light constraint to implement id, but require more complicated machinery for e.g. ***. In this case, you're strictly speaking working with two different categories: the one described by the Category instance, and a smaller subcategory of it that's cartesian monoidal. Or even a whole family of categories, each with a different PairObject-connected class of objects.

As to why Monoid: as you've guessed, it's not really the right class for the task, but it does the job and is widespread. Your ProperUnit class wouldn't give you any more tooling, as the toUnitType method is always trivial and fromUnitType ≡ const mempty. I believe what you're actually thinking about here is

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

but that's awkward to do without dependent types. I'm also not sure whether it would actually buy us anything.

Unfortunately the name Monoid makes it a bit of a red herring in this context.

The “job” it solves, concretely, is concerned with global elements, in particular when using the Agent types for encoding categorical composition chains into lambda expressions – all of it in the footsteps of Conal Elliot's work on hardware compilation etc., but as a Haskell library.

I shuffled around what's the best place for putting the various constraints a couple of times, and the commented-out PairObject k (UnitObject k) (UnitObject k) constraints are an artifact of that: these constraints should morally hold, but what I found was that explicitly requiring them there causes more problems when defining instances, than it solves when using them.

Recommended topics

Hot tags