Как определить, бесконечен ли список?

Ответ 1

Применение length к неизвестным спискам - это, как правило, плохая идея, как из-за бесконечных списков, так и из-за концептуально, потому что часто оказывается, что вы все равно не заботитесь о длине.

Вы сказали в комментарии:

Я очень новичок в Haskell, так что теперь, не бесконечные структуры делают мои программы очень уязвимыми?

Не совсем. Хотя некоторые из нас желают, чтобы были лучшие способы различать обязательно конечные и обязательно бесконечные данные, вы всегда будете в безопасности при создании, обработке и анализе ленивых структур постепенно. Вычисление длины явно не инкрементально, но проверка того, является ли длина выше или ниже некоторого значения отсечки, и очень часто, что все, что вы хотели сделать в любом случае!

Тривиальный случай - это тестирование для непустых списков. isNonEmpty xs == length xs > 0 является плохой реализацией, потому что он рассматривает неограниченное количество элементов, при рассмотрении одного из них будет достаточно! Сравните это:

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

Это не только безопасно применять к бесконечному списку, но и намного эффективнее в конечных списках - требуется только постоянное время, а не время, линейное по длине списка. Это также как реализована стандартная библиотечная функция null.

Чтобы обобщить это для тестирования длины относительно отсечки, вам, очевидно, нужно будет рассмотреть как можно больше списка, чем длина, с которой вы сравниваете. Мы можем сделать именно это и не более, используя стандартную библиотечную функцию drop:

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

Учитывая длину n и (возможно, бесконечный) список xs, это исключает первые n элементы xs, если они существуют, а затем проверяет, не является ли результат непустым. Поскольку drop создает пустой список, если n больше, чем длина списка, это работает правильно для всех положительных n (увы, нет неотрицательного целочисленного типа, например натуральных чисел, в стандартных библиотеках).

Ключевым моментом здесь является то, что в большинстве случаев лучше думать о списках как итеративных потоках, а не о простой структуре данных. Когда это возможно, вы хотите делать такие вещи, как преобразование, накопление, усечение и т.д., И либо создавать другой список в качестве вывода, либо анализировать только известную конечную сумму списка, а не пытаться обрабатывать весь список за один раз.

Если вы используете этот подход, ваши функции будут работать не только в конечных и бесконечных списках, но они также получат больше пользы от лень и оптимизатора GHC и, скорее всего, будут работать быстрее и использовать меньше памяти.

Ответ 2

Проблема с остановкой была впервые доказана неразрешимой, если предположить, что существует Oracle Halting, а затем написать функцию, которая сделала противоположное тому, что сказал оракул бывает. Позвольте воспроизвести это здесь:

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

Теперь мы хотим сделать список impossibleList, который делает противоположное тому, что говорит isInfinite. Итак, если impossibleList бесконечно, оно фактически [], и если оно не бесконечно, оно 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

Попробуйте сами в ghci с isInfinite = const True и isInfinite = const False.

Ответ 3

isInfinite x = length x `seq` False

Ответ 4

Нам не нужно решать проблему остановки, чтобы безопасно называть "длину". Мы просто должны быть консервативными; принять все, что имеет доказательство конечности, отвергнуть все, что не имеет (включая множество конечных списков). Это именно то, для каких систем типов, поэтому мы используем следующий тип (t - это наш тип элемента, который мы игнорируем):

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

Конечный класс будет содержать только конечные списки, поэтому проверка типов гарантирует, что мы имеем конечный аргумент. членство в Finite будет нашим доказательством конечности. Функция toList просто превращает конечные значения в обычные списки Haskell:

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

Теперь, каковы наши экземпляры? Мы знаем, что пустые списки конечны, поэтому мы представляем их тип данных:

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

Если "минус" элемент в конечный список, мы получаем конечный список (например, "x: xs" конечен, если "xs" конечен):

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

Любой, вызывающий нашу функцию terminatingLength, должен теперь доказать, что их список конечен, иначе их код не будет компилироваться. Это не устранило проблему проблемы с остановкой, но мы переместили ее на время компиляции, а не на время выполнения. Компилятор может зависать, пытаясь определить членство в Finite, но это лучше, чем наличие производственной программы зависает, когда она дает некоторые неожиданные данные.

Слово предостережения: полиморфизм Haskell "ad-hoc" допускает, чтобы в других точках кода допускалось довольно много произвольных экземпляров Finite, и terminatingLength будет принимать их как доказательства конечности, даже если они не являются. Это не так уж плохо; если кто-то пытается обойти механизмы безопасности вашего кода, они получают ошибки, которых они заслуживают;)

Ответ 5

Нет - вы можете в лучшем случае оценить. См. Проблема с остановкой.

Ответ 6

Существует также возможность разделения конечных и бесконечных списков по дизайну и использования для них разных типов.

К сожалению, Haskell (в отличие от Agda, например) не позволяет вам гарантировать, что структура данных всегда конечна, вы можете использовать методы общее функциональное программирование, чтобы гарантировать это.

И вы можете объявлять бесконечные списки (потоки AKA) как

data Stream a = Stream a (Stream a)

который не имеет никакого способа завершить последовательность (это в основном список без []).