sobre - multiplos en haskell
Habitantes no enteros de enteros en Haskell (2)
Bueno, hay Succ _|_ , Succ (Succ _|_) etc. Sin embargo, puede haber incluido esos entre los ''valores de fondo''. inf = Succ inf se suele llamar infinity o omega (como el ordinal de los números naturales).
Números naturales de Peano en Haskell definidos como data Peano = Zero | Succ Peano data Peano = Zero | Succ Peano son bestias bastante extrañas: además de naturales y valores de fondo, hay un "infinito entero" inf = Succ inf entre ellos.
¿Hay otros habitantes del tipo Peano ? ¿Este número infinito tiene un nombre?
No son extraños, simplemente son naturales coinductivos . Dejando de lado el problema de ⊥, podemos definir el tipo de número natural aquí como consistente en Zero o Succ aplicado a un número natural. Una definición inductiva supondría un final bien definido, es decir, que cualquier número comienza desde un constructor Zero . La definición coinductiva simplemente dice que dado cualquier número natural, será Zero o podemos eliminar el Succ externo para obtener otro número natural.
La diferencia aparentemente sutil es que la definición coinductiva incluye una serie interminable de constructores de Succ , que en realidad es una verdadera representación del infinito. Esto es significativo porque, si bien una definición inductiva se trata de garantizar que la recursión alcance un caso base bien definido, las definiciones coinductivas consisten en garantizar que siempre haya un próximo paso bien definido disponible.
La interpretación coinductiva es conveniente y, de alguna manera, obligatoria en Haskell, debido a que los constructores de datos son flojos.
Entonces, este número infinito realmente es infinito, o ω si necesitas especificar qué infinito, como dijo Daniel Fischer. Es solo un infinito coinductivo, muy parecido a las listas infinitas que se encuentran más comúnmente.
Si piensas en los números naturales a través de la codificación de su iglesia, los números finitos significan "iterar esta función N veces"; ω significa "iterar esta función indefinidamente".