[smabie]

Assuming non-fixed width integers, how can you have an infinite sum type?

[tel]

There’s nothing wrong with an infinite sum, in principle. You can’t usually define them unless you can use recursion. In the case of integers you can do

    data Int = Positive Nat | Negative Nat
    data Nat = Zero | Succ Nat

[jolmg]

Though, that has 2 zeros, a positive and a negative one, but zero should be neither. To avoid that, you can do:

  data Int = Zero | NonZero Sign PositiveInt
  data PositiveInt = One | Succ PositiveInt
  data Sign = Positive | Negative

[tel]

Good point.

[arianvanp]

You can't. The Natural number definition combines a sum type with a recursive position. Or in other words, a finite tag (either zero or successors, 2 options) plus a pointer to the next value in the case of successor.