n923263

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.

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.)

Hell, a significant number of us have strong opinions about the visual shape of (fixed-font, usually monospaced) text in our code (eg, the various indentation style wars) or prose (eg, Knuth et al's anti-river typesetting algorithms).

To be fair, that's just begging for the XML in the comment block to get out of sync with the actual regex literal.

Minor erratum: "1.1 (binary) × 2^8 is 304" should be 384.