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?
1
-
$\begingroup$ You have cardinal(A+B)=cardinal(A)+cardinal(B), and you can check that cardinal is in fact a monoid morphism. $\endgroup$– xavierm02Apr 3, 2020 at 11:11
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
4
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.
-
$\begingroup$ 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? $\endgroup$– al palApr 4, 2020 at 19:30
-
1$\begingroup$ @al-pal: I don't quite understand your question. You could define
type TWO = A + Bandtype THREE = C + D + Eand then the sum typeTWO + THREEwould have five possible type constructors, corresponding toA,B,C,DorE, which you could case split on. Does this help? $\endgroup$– varkorApr 4, 2020 at 20:47 -
$\begingroup$ 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. $\endgroup$– al palApr 4, 2020 at 22:27
-
1$\begingroup$ If
Xis a specific type, then a polynomialX * X + X + 1corresponds to a type (either a pair ofXs, a singleXor 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 tocase,matchorswitchin the type theory; and the piecewise notation in typical mathematics. $\endgroup$– varkorApr 4, 2020 at 22:54