# Is there any correspondence between SUM type in type theory and arithmetical summation?

Is there any correspondence between the coproduct(sum) type in type theory and arithmetical summation?

For example what does 3+4 or x+6 mean in type theory?

• You have cardinal(A+B)=cardinal(A)+cardinal(B), and you can check that cardinal is in fact a monoid morphism. – xavierm02 Apr 3 at 11:11

## 1 Answer

The arithmetic notation in type theory is motivated by the behaviour on sets, where the disjoint union $$A + B$$ has $$|A| + |B|$$ elements; the cartesian product has $$|A| \times |B|$$ elements; and the set of functions $$B^A$$ has $$|B|^{|A|}$$ elements. Sum, product and function types satisfy many of the usual identities you expect of arithmetic (although typically up to isomorphism, rather than equality).

The paper Objects of Categories as Complex Numbers by Marcelo Fiore and Tom Leinster explores this in some detail, though it helps to have a little experience with algebra or category theory.

Sometimes a natural number $$n$$ will denote a type with exactly $$n$$ terms in any context (analogous to a set with $$n$$ elements). In this setting, $$3 + 4 \cong 7$$ as types. $$x + 6$$ isn't well-formed without placing $$x$$ in some context.

• Thanks a lot for your answer. So you are saying there is no interpretation of arithmetical 2+3 that involves case analysis as what we have for coproduct types? – al pal Apr 4 at 19:30
• @al-pal: I don't quite understand your question. You could define type TWO = A + B and type THREE = C + D + E and then the sum type TWO + THREE would have five possible type constructors, corresponding to A, B, C, D or E, which you could case split on. Does this help? – varkor Apr 4 at 20:47
• Well, I'm trying to look at this thing the other way around and from the arithmetic point of view, that means I thought when we define a polynomial, in a way we are programming a function and in this language + is the case statement. I might be wrong or confused about the similarities between + is arithmetic and type theory. – al pal Apr 4 at 22:27
• If X is a specific type, then a polynomial X * X + X + 1 corresponds to a type (either a pair of Xs, a single X or nothing). Here + represents "or", which can be considered the disjoint union of sets. Adding and multiplying polynomials of types acts in the same way you would add and multiply polynomials of integers. Case-splitting corresponds to case, match or switch in the type theory; and the piecewise notation in typical mathematics. – varkor Apr 4 at 22:54