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

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

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.

Нам не нужно решать проблему остановки, чтобы безопасно вызывать 'length'. Нам просто нужно быть консервативными; принять все, что имеет доказательство конечности, отвергнуть все, что нет (включая множество конечных списков). Именно для этого и нужны системы типов, поэтому мы используем следующий тип (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

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

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

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

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

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

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

data Stream a = Stream a (Stream a)

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