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

Question

Есть ли способ узнать, бесконечен ли список в Хаскеле? Причина в том, что я не хочу применять такие функции, как length, к бесконечным спискам.

Answer 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, а также с большей вероятностью работать быстрее и использовать меньше памяти.

Answer 2

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

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.

Answer 3

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

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

Класс Finite будет содержать только конечные списки, поэтому проверка типовбудет гарантировать, что у нас есть конечный аргумент.членство в 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, должен теперь доказать, что их список конечен, иначе их код не скомпилируется.Это не устранило проблему Halting Problem, но мы переместили ее на время компиляции, а не времени выполнения.При попытке определить членство в Finite компилятор может зависнуть, но это лучше, чем зависание производственной программы, когда ему выдаются непредвиденные данные.

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

Answer 4

isInfinite x = length x `seq` False

Answer 5

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

Answer 6

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

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

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

data Stream a = Stream a (Stream a)

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