# 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
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 1, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.7788063287734985, "perplexity": 622.310627652191}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2021-21/segments/1620243989705.28/warc/CC-MAIN-20210512193253-20210512223253-00094.warc.gz"}