list - tag - mailchimp personalized name

¿Cómo saber si una lista es infinita?

Question

¿Hay alguna forma de saber si una lista en Haskell es infinita? La razón es que no quiero aplicar funciones como la length a listas infinitas.

Answer 1

Aplicar length a listas desconocidas generalmente es una mala idea, tanto debido a listas infinitas como conceptualmente porque a menudo resulta que en realidad no te importa la longitud de todos modos.

Usted dijo en un comentario:

Soy muy nuevo en Haskell, así que ahora, ¿las estructuras infinitas no hacen que mis programas sean muy vulnerables?

Realmente no. Mientras que algunos de nosotros deseamos que haya mejores formas de distinguir entre datos necesariamente finitos y necesariamente infinitos, siempre estás seguro cuando creas , procesas y examinas las estructuras perezosas de forma incremental . La computación de la duración es claramente no incremental, pero verificando si la longitud está por encima o por debajo de algún valor de corte es , ¡y muy a menudo eso es todo lo que querías hacer de todos modos!

Un caso trivial es la prueba de listas no vacías. isNonEmpty xs == length xs > 0 es una implementación incorrecta porque examina una cantidad ilimitada de elementos, ¡cuando el examen de uno solo sería suficiente! Compare esto:

isNonEmpty [] = False
isNonEmpty (_:_) = True

No solo es seguro aplicarlo a una lista infinita, sino que también es mucho más eficiente en listas finitas: solo lleva tiempo constante, en lugar de tiempo lineal en la longitud de la lista. También es así como se implementa la función de biblioteca estándar null .

Para generalizar esto para la prueba de longitud en relación con un punto de corte, obviamente deberá examinar tanto de la lista como la longitud con la que compara. Podemos hacer exactamente esto, y nada más, utilizando la función de biblioteca estándar drop :

longerThan :: Int -> [a] -> Bool
longerThan n xs = isNonEmpty $ drop n xs

Dada una longitud n una lista (posiblemente infinita) xs , esto elimina los primeros n elementos de xs si existen, luego verifica si el resultado es no vacío. Debido a que drop produce la lista vacía si n es mayor que la longitud de la lista, esto funciona correctamente para todos los n positivos (¡ay !, no hay ningún tipo entero no negativo, por ejemplo, números naturales, en las bibliotecas estándar).

El punto clave aquí es que es mejor en la mayoría de los casos pensar en listas como flujos iterativos, no en una estructura de datos simple. Cuando sea posible, debe hacer cosas como transformar, acumular, truncar, etc., y producir otra lista como resultado o examinar solo una cantidad finita conocida de la lista, en lugar de tratar de procesar toda la lista de una vez.

Si usa este enfoque, sus funciones no solo funcionarán correctamente en listas finitas e infinitas, sino que también se beneficiarán más de la pereza y del optimizador de GHC, y es probable que corran más rápido y utilicen menos memoria.

Answer 2

El problema de la detención se demostró por primera vez irresolubles al asumir que existía un Oráculo de Detención, y luego escribir una función que hacía lo contrario de lo que el oráculo dijo que sucedería. Vamos a reproducir eso aquí:

isInfinite :: [a] -> Bool
isInfinite ls = {- Magic! -}

Ahora, queremos hacer una lista impossibleList que haga lo contrario de lo que isInfinite dice que debería. Entonces, si lista impossibleList es infinita, en realidad es [] , y si no es infinita, es something : impossibleList .

-- using a string here so you can watch it explode in ghci
impossibleList :: [String]
impossibleList =
case isInfinite impossibleList of
True -> []
False -> "loop!" : impossibleList

Pruébelo usted mismo en ghci con isInfinite = const True e isInfinite = const False .

Answer 3

No necesitamos resolver el problema de detención para llamar a ''longitud'' de forma segura. Solo debemos ser conservadores; acepte todo lo que tenga una prueba de finitud, rechace todo lo que no lo haga (incluidas muchas listas finitas). Esto es exactamente para lo que son los sistemas de tipo, entonces usamos el siguiente tipo (t es nuestro tipo de elemento, que ignoramos):

terminatingLength :: (Finite a) => a t -> Int
terminatingLength = length . toList

La clase finita solo contendrá listas finitas, por lo que el verificador de tipos asegurará que tengamos un argumento finito. la membresía de Finite será nuestra prueba de finitud. La función "toList" simplemente convierte los valores finitos en listas regulares de Haskell:

class Finite a where
toList :: a t -> [t]

Ahora, ¿cuáles son nuestras instancias? Sabemos que las listas vacías son finitas, por lo que creamos un tipo de datos para representarlas:

-- Type-level version of "[]"
data Nil a = Nil
instance Finite Nil where
toList Nil = []

Si ''contramos'' un elemento en una lista finita, obtendremos una lista finita (por ejemplo, "x: xs" es finito si "xs" es finito):

-- Type-level version of ":"
data Cons v a = Cons a (v a)
-- A finite tail implies a finite Cons
instance (Finite a) => Finite (Cons a) where
toList (Cons h t) = h : toList t -- Simple tail recursion

Cualquiera que llame a nuestra función terminatingLength ahora debe probar que su lista es finita, de lo contrario su código no se compilará. Esto no ha eliminado el problema del problema de detención, pero lo hemos cambiado al tiempo de compilación en lugar del tiempo de ejecución. El compilador puede bloquearse al intentar determinar la pertenencia a Finite, pero eso es mejor que tener un programa de producción bloqueado cuando se le dan algunos datos inesperados.

Una advertencia: el polimorfismo "ad-hoc" de Haskell permite que se declaren instancias de Finite prácticamente arbitrarias en otros puntos del código, y terminatingLength las aceptará como pruebas de finitud, incluso si no lo son. Esto no es tan malo; si alguien intenta eludir los mecanismos de seguridad de tu código, obtienen los errores que merecen;)

Answer 4

No, en el mejor de los casos puede estimar. Ver el problema de detención .

Answer 5

También existe la posibilidad de separar listas finitas e infinitas por diseño y usar distintos tipos para ellas.

Desafortunadamente, Haskell (a diferencia de Agda por ejemplo) no le permite hacer cumplir que una estructura de datos siempre es finita, puede emplear técnicas de programación funcional total para garantizar eso.

Y puede declarar listas infinitas (AKA streams) como

data Stream a = Stream a (Stream a)

que no tiene forma de cómo terminar una secuencia (básicamente es una lista sin [] ).

Answer 6

isInfinite x = length x `seq` False