Non-integer inhabitants of integers in Haskell

Question

Peano natural numbers in Haskell defined as data Peano = Zero | Succ Peano are quite strange beasts: besides plain naturals and bottom values, there is an "infinite integer" inf = Succ inf among them.

Are there any other inhabitants of the Peano type? Does this infinite number has a name?

Answer 1

They're not strange, they're simply coinductive naturals. Leaving aside the issue of ⊥, we can define the natural number type here as consisting of either Zero, or Succ applied to a natural number. An inductive definition would assume a well-defined end, i.e., that any number starts from a Zero constructor. The coinductive definition merely says that given any natural number, it will either be Zero or we can remove the outer Succ to get another natural number.

The seemingly subtle difference there is that the coinductive definition includes an endless series of Succ constructors, which really is a true representation of infinity. This is meaningful because, while an inductive definition is about ensuring that recursion will reach a well-defined base case, coinductive definitions are about ensuring that there will always be a well-define next step available.

The coinductive interpretation is convenient and in some ways obligatory in Haskell, due to data constructors being lazy.

So, this infinite number really is infinity, or ω if you need to specify which infinity, as Daniel Fischer said. It's just a coinductive infinity, much like the infinite lists that are more commonly encountered.

If you think of natural numbers via their church encoding, finite numbers mean "iterate this function N times"; ω means "iterate this function indefinitely".