Они не странные, они просто коиндуктивные натуралы. Оставляя в стороне вопрос о ⊥, мы можем определить тип натурального числа здесь как состоящий из Zero или Succ, примененного к натуральному числу. Индуктивное определение предполагает четко определенный конец, т. Е. Любое число начинается с конструктора Zero. В коиндуктивном определении просто говорится, что для любого натурального числа это будет либо Zero, либо мы можем удалить внешнее Succ, чтобы получить другое натуральное число.
На первый взгляд, едва заметное различие заключается в том, что коиндуктивное определение включает в себя бесконечный ряд конструкторов Succ, который действительно является истинным представлением бесконечности. Это имеет смысл, потому что, хотя индуктивное определение касается обеспечения того, чтобы рекурсия достигла четко определенного базового случая, коиндуктивные определения означают, что всегда будет доступен четко определенный следующий шаг.
Коиндуктивная интерпретация удобна и в некоторых отношениях обязательна в Haskell, поскольку конструкторы данных ленивы.
Итак, это бесконечное число на самом деле является бесконечностью, или ω, если вам нужно указать, какая бесконечность, как сказал Даниэль Фишер. Это просто коиндуктивная бесконечность, очень похожая на бесконечные списки, которые встречаются чаще.
Если вы думаете о натуральных числах через их церковное кодирование, конечные числа означают «повторить эту функцию N раз»; ω означает «повторять эту функцию до бесконечности».