Search code examples
computer-sciencetype-theorycomputer-science-theory

Is the type product (tuple) operator associative?


For example, given the types A, B and C: is A×B×C=(A×BC=A×(B×C) true, or is the tuple always 'flattened out'? Intuition would tell me that it is associative, but on the other hand that would mean tuples of tuples aren't possible. I have found no mention of the properties of the type product operator in any resources I can find - the Wikipedia page describes product types but doesn't go into great detail about the operator itself.


Solution

  • Technically, it would be associative, but it depends a bit on how you are using it and how much you want (or need) to adhere to its definition. In many type systems, you only have two-type tuples, and every product type that contains more than two types is just two-type tuple where one of the types is another 2-type tuple: (A, B, C) ~= ((A, B), C) or (A, B, C) ~= (A, (B, C)). Now which of these two you end up with depends on your definition. A simple left-to-right parsing would probably end up with the latter version.

    But in the end, it doesn’t really matter. Since this is about type theory, the types are always exactly known; so a tuple of a tuple couldn’t contain some “unknown” tuple. That inner tuple’s types would be known too. And when you know the types, and you know that there is a tuple of tuples, there is not really a difference between (A, B, (C, D, E)) and (A, B, C, D, E). After all, you know where that “inner tuple” begins and ends. And if the type system requires you to make it (A, (B, (C, (D, E)))), then that’s not really a problem either.