Can we think of a non-symmetric product type in Haskell?

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 Control.Category.Constrained.CoCartesian).

• regroup and regroup' are for (a, (b, c)) ≅ ((a, b), c);
• attachUnit and detachUnit are for 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?

• The product of types is necessarily symmetric, because you can always swap with (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. – varkor Sep 23 '20 at 15:26
• @varkor what is a tensor product and how is it different from simply product? Can you give an example of a non-symmetric tensor product, please? – Zhiltsoff Igor Sep 23 '20 at 15:30
• A (cartesian) product is a particular kind of tensor product that has projections $A \otimes B \to A$ and $A \otimes B \to B$, which satisfy a universal property). I realised that I don't think Haskell is able to express the examples of noncommutative type operators (without, say, type-level lambdas), so I don't have an answer to your question. I just wanted to clarify the terminology. – varkor Sep 23 '20 at 15:54
• @varkor I suppose we can use the A ⊗ B -> A and A ⊗ B -> B arrows 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? – Zhiltsoff Igor Sep 25 '20 at 9:23
• For example, if we can write arbitrary functions at the type level, then we can declare a type operator $\lambda (A, B) . \mathsf{if}\ A = \mathsf{Void}\ \mathsf{then}\ B\ \mathsf{else}\ A$, i.e. a type operator that is always equal to the left operand, unless the left operand is the empty type. This has the empty type for a unit, and is associative, but is clearly not symmetric. – varkor Sep 26 '20 at 18:44