Comment savoir si une liste est infinie?

Question

Existe-t-il un moyen de savoir si une liste dans Haskell est infinie?La raison est que je ne veux pas appliquer des fonctions telles que length à des listes infinies.

Answer 1

Appliquer length à des listes inconnues est généralement une mauvaise idée, à la fois pratiquement en raison de listes infinies, et conceptuellement parce que souvent il s'avère que vous ne vous souciez pas vraiment de la longueur de toute façon.

Vous avez dit dans un commentaire:

Je suis très nouveau dans Haskell, alors maintenant, des structures infinies ne rendent-elles pas mes programmes très vulnérables?

Pas vraiment. Alors que certains d'entre nous souhaiteraient qu'il y ait de meilleures façons de faire la distinction entre les données nécessairement finies et nécessairement infinies, vous êtes toujours en sécurité lorsque vous créez , traitez et examinez structures paresseuses de manière incrémentielle . Le calcul de la longueur n'est clairement pas incrémental, mais vérifier si la longueur est au-dessus ou en dessous d'une certaine valeur limite est , et très souvent c'est tout ce que vous vouliez faire de toute façon!

Un cas trivial est le test des listes non vides. isNonEmpty xs == length xs > 0 est une mauvaise implémentation car il examine un nombre illimité d'éléments, alors qu'en examiner un seul suffirait! Comparez ceci:

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

Non seulement cela est sûr à appliquer à une liste infinie, mais c'est aussi beaucoup plus efficace sur les listes finies - cela ne prend que du temps constant, au lieu d'un temps linéaire dans la longueur de la liste. C'est aussi comment le standard La fonction de bibliothèque null est implémentée .

Pour généraliser cela pour les tests de longueur par rapport à un seuil, vous devrez évidemment examiner autant la liste que la longueur à laquelle vous comparez. Nous pouvons faire exactement cela, et rien de plus, en utilisant la fonction de bibliothèque standard drop:

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

Étant donné une longueur n et une liste (éventuellement infinie) xs, cela supprime les premiers éléments n de xs s'ils existent, puis vérifie si le résultat n'est pas vide. Parce que drop produit la liste vide si n est plus grand que la longueur de la liste, cela fonctionne correctement pour tous les n positifs (hélas, il n'y a pas de type entier non négatif, par exemple les nombres naturels, dans les bibliothèques standard).

---

Le point clé ici est qu'il vaut mieux dans la plupart des cas considérer les listes comme des flux itératifs, pas comme une simple structure de données. Lorsque cela est possible, vous voulez faire des choses comme transformer, accumuler, tronquer, etc., et soit produire une autre liste en sortie, soit examiner uniquement une quantité finie connue de la liste, plutôt que d'essayer de traiter la liste entière en une seule fois.

Si vous utilisez cette approche, non seulement vos fonctions fonctionneront correctement sur des listes finies et infinies à la fois, mais elles bénéficieront également davantage de la paresse et de l'optimiseur de GHC, et seront susceptibles de fonctionner plus rapidement et utilise moins de mémoire.

Answer 2

Le problème d'arrêt a d'abord été prouvé insoluble en supposant qu'un Oracle d'arrêt existait, puis en écrivant une fonctioncela a fait le contraire de ce que cet oracle a dit arriverait.Reproduisons cela ici:

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

Maintenant, nous voulons faire une liste impossibleList qui fait le contraire de ce que isInfinite dit qu'il devrait.Donc, si impossibleList est infini, c'est en fait [], et s'il n'est pas infini, c'est 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

Essayez-le vous-même dans ghci avec isInfinite = const True et isInfinite = const False.

Answer 3

isInfinite x = length x `seq` False

Answer 4

Nous n'avons pas besoin de résoudre le problème d'arrêt pour appeler «length» en toute sécurité. Nous devons simplement être conservateurs; accepter tout ce qui a une preuve de finitude, rejeter tout ce qui ne l'est pas (y compris de nombreuses listes finies). C'est exactement à quoi servent les systèmes de types, nous utilisons donc le type suivant (t est notre type d'élément, que nous ignorons):

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

La classe Finite ne contiendra que des listes finies, donc le vérificateur de type s'assurera que nous avons un argument fini. l'appartenance à Finite sera notre preuve de finitude. La fonction "toList" transforme simplement les valeurs finies en listes Haskell régulières:

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

Maintenant, quelles sont nos instances? Nous savons que les listes vides sont finies, nous créons donc un type de données pour les représenter:

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

Si nous 'contre' un élément sur une liste finie, nous obtenons une liste finie (par exemple, "x: xs" est fini si "xs" est fini):

-- 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

Quiconque appelle notre fonction terminatingLength doit maintenant prouver que sa liste est finie, sinon son code ne sera pas compilé. Cela n'a pas supprimé le problème du problème d'arrêt, mais nous l'avons déplacé au moment de la compilation plutôt qu'au moment de l'exécution. Le compilateur peut se bloquer en essayant de déterminer l'appartenance à Finite, mais c'est mieux que d'avoir un programme de production bloqué lorsqu'il reçoit des données inattendues.

Un mot d'avertissement: le polymorphisme «ad hoc» de Haskell permet à des instances assez arbitraires de Finite d'être déclarées à d'autres points du code, et terminatingLength les acceptera comme des preuves de finitude même si ce n'est pas le cas. Ce n'est pas trop mal cependant; si quelqu'un essaie de contourner les mécanismes de sécurité de votre code, il obtient les erreurs qu'il mérite;)

Answer 5

Non - vous pouvez au mieux faire une estimation.Consultez le problème d'arrêt .

Answer 6

Il y a aussi la possibilité de séparer des listes finies et infinies par conception et d'utiliser des types distincts pour elles.

Malheureusement, Haskell (contrairement à Agda par exemple) ne vous permet pasfaire en sorte qu'une structure de données soit toujours finie, vous pouvez utiliser des techniques de programmation fonctionnelle totale pour garantir cela.

Et vous pouvez déclarer des listes infinies (flux AKA) comme

data Stream a = Stream a (Stream a)

qui n'a aucun moyen de terminer une séquence (c'est essentiellement une liste sans []).