If it weren't for finiteness restrictions, you could write the following in Haskell and it'd make a natural number type that acted basically as expected.
data Zero = Zero
data One = One
data Two = Two
...
data NaturalNumber = Zero | One | Two | Three | ...
Whatever you would say about sets, you might as well say the same thing about types; the distinction in terminology doesn't amount to much. The natural numbers are the disjoint union of {0}, {1}, {2}, {3}, ... . They're also the disjoint union of the even naturals and the odd naturals, or the disjoint union of {0}, {1}, primes, and composites. There are a million ways in which they are a disjoint union.
data Zero = Zero data One = One data Two = Two ... data NaturalNumber = Zero | One | Two | Three | ...
Whatever you would say about sets, you might as well say the same thing about types; the distinction in terminology doesn't amount to much. The natural numbers are the disjoint union of {0}, {1}, {2}, {3}, ... . They're also the disjoint union of the even naturals and the odd naturals, or the disjoint union of {0}, {1}, primes, and composites. There are a million ways in which they are a disjoint union.