Pairs in general (ie binary products) are always sums. A pair type `X * Y` is a multiplication, which is equivalent to `enum {Y y_x0,Y y_x1,Y y_x2,...}` or `Y + Y + Y + ...`, effectively a sum type where the descriminant of the enum is a X, and each case of the enum contains a Y. This is equivalent to how 3 * 7 = 7 + 7 + 7, where you have three terms of size seven.
Similarly, functions in general (ie (binary) exponentiations) are always products. A function type `X -> Y` (or `Y ^ X`) is a exponentiation, which is equivalent to `struct {Y y_x0,Y y_x1,Y y_x2,...}` or `Y * Y * Y * ...`, effectively a product (or latent array) type where the index of the 'array' is a X, and each element of the 'array' is a Y. This is equivalent to how 7 ^ 3 = 7 * 7 * 7, where you have three factors of size seven. (Note that functions have the exponent/argument first and the base/result second.)
All of the above applies without dependent types. Dependent types let the `Y` type depend on which value of type X is involved. (That is, the Y type depends on the X value.)
Aha, thanks!
A good mnemonic is that that if X and Y are finite types[0], sum, product and exponent types are just doing the relevant arithmetic on the types.
(Bool->Bool,Uint8+()) is just a verbose way of saying (2^2 * (256+1)), where 1,2, and 256 are types with the appropriate number of elements.
The cases involving infinite types are just a (straightforward?) generalization of that.
0: eg 0=noreturn [1],1=void,2=Bool,256=uint8_t
1: Much like in set theory, zero is the empty set.