Естественные числа Пеано в Хаскелле, определенные как data Peano = Zero | Succ Peano, являются довольно странными животными: помимо простых естественных и нижних значений между ними существует "бесконечное целое число" inf = Succ inf.
Есть ли другие жители типа Peano? Имеет ли это бесконечное число имя?
Они не странные, они просто коиндуктивные naturals. Оставив в стороне проблему ⊥, мы можем определить здесь тип натурального числа, состоящий либо из Zero, либо Succ, примененного к натуральному числу. Индуктивное определение предполагало бы четко определенный конец, т.е. Что любое число начинается с конструктора Zero. Коиндуктивное определение просто говорит, что при любом натуральном числе оно будет либо Zero, либо мы можем удалить внешний Succ, чтобы получить другое натуральное число.
По-видимому, тонкая разница в том, что коиндуктивное определение включает бесконечную серию конструкторов Succ, которая на самом деле является истинным представлением бесконечности. Это имеет смысл, потому что, хотя индуктивное определение заключается в обеспечении того, что рекурсия достигнет четко определенного базового случая, коиндуктивные определения состоят в обеспечении того, что всегда будет хорошо определен следующий следующий шаг.
Коиндуктивная интерпретация удобна и в некотором смысле обязательна в Haskell, поскольку конструкторы данных ленивы.
Итак, это бесконечное число действительно бесконечно, или ω, если вам нужно указать, какую бесконечность, как сказал Даниэль Фишер. Это просто коиндуктивная бесконечность, очень похожая на бесконечные списки, которые чаще встречаются.
Если вы думаете о натуральных числах посредством их церковного кодирования, конечные числа означают "итерировать эту функцию N раз"; ω означает "итерировать эту функцию неограниченно".
Ну, есть Succ _|_, Succ (Succ _|_) и т.д. Возможно, вы включили те из "нижних значений". inf = Succ inf обычно называется infinity или omega (как порядковый номер натуральных чисел).