For example, given the types A, B and C: is A×B×C=(A×B)×C=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.
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.