4 ms·

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 da

by tel 7y ago

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 7y ago
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 7y ago
  Good point.