0
$\begingroup$

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?

Improve this question
$\endgroup$
9
  • $\begingroup$ 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. $\endgroup$
    – varkor
    Sep 23, 2020 at 15:26
  • $\begingroup$ @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? $\endgroup$
    – Zhiltsoff Igor
    Sep 23, 2020 at 15:30
  • $\begingroup$ 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. $\endgroup$
    – varkor
    Sep 23, 2020 at 15:54
  • $\begingroup$ @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? $\endgroup$
    – Zhiltsoff Igor
    Sep 25, 2020 at 9:23
  • 1
    $\begingroup$ 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. $\endgroup$
    – varkor
    Sep 26, 2020 at 18:44

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.