Meta note: I asked this question here a while ago. It got an answer:
type a /\!! b = (a, ((b -> Void) -> Void))
Unfortunately, I do not reckon it to be quite right:
() /\!! a ≅ a does not hold.
I do not want to delete the question on Stack Overflow as the answerer still put quite some effort in (and I did not manage to migrate it here). I will close it as a duplicate, if I get the fitting answer here, if that's alright. We discussed this issue on Meta.SE.
Control.Category.Constrained.Cartesian is a class for monoidal categories with some natural transformations (the product is
(,) and the unit defaults to
(); the product cannot be changed, unlike the sum in
(a, (b, c)) ≅ ((a, b), c);
a ≅ (a, unit).
They almost give us the monoid. The only thing that is left is
(unit, a) ≅ a. Here we use
(,) being symmetrical:
(a, b) ≅ (b, a).
As far as I know, it is not a general property. Bartosz Milewski attributes the property to symmetrical monoidal categories (for example, here).
Is there some product type in Haskell which is not symmetrical?
(b, a), as you mention. However, there are many tensor products of types that are nonsymmetric: take any associative non-commutative binary type operator. If this type operator has a unit, then it will form a nonsymmetric monoidal category. $\endgroup$
A ⊗ B -> Aand
A ⊗ B -> Barrows to get
A ⊗ B -> (B, A). But is it generally true that we have an arrow back (using the properties you wrote about)? Is it true for such products in Haskell? $\endgroup$