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:
Cartesian
extends Category
.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?1 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.
1 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->Type
s 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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With