Does it help if I tell you that types form a semiring[0]? Note that the natural numbers also form a semiring (with 0 as the additive identity and 1 as the mult

Does it help if I tell you that types form a semiring[0]? Note that the natural numbers also form a semiring (with 0 as the additive identity and 1 as the multiplicative identity). The natural numbers can be embedded in the semiring of types, but they are a strict subset - there are types that don't correspond to natural numbers (which addressed the point on the great-grandparent post). There's a great paper by Fiore and Leinster[1] called "Objects of Categories as Complex Numbers" which shows how you can treat elements of some semirings as complex numbers for the purposes of proving arithmetic statements about them, and then convert the proofs that use complex numbers into valid proofs in the semiring. [0] http://en.wikipedia.org/wiki/Semiring http://en.wikipedia.org/wiki/Semiring [1] http://arxiv.org/abs/math/0212377 http://arxiv.org/abs/math/0212377