Являются ли списки индуктивными или коиндуктивными в Haskell?

Итак, я немного читал о coinduction в последнее время, и теперь мне интересно: являются ли списки Haskell индуктивными или коиндуктивными? Я также слышал, что Haskell не отличает этих двух, но если да, то как они делают это формально?

Списки определяются индуктивно, data [a] = [] | a : [a], но могут использоваться коиндуктивно, ones = a:ones. Мы можем создавать бесконечные списки. Тем не менее, мы можем создавать конечные списки. Итак, каковы они?

Связано это в Идрисе, где тип List a является строго индуктивным типом и, следовательно, является только конечным списком. Он определен сродни тому, как он находится в Хаскелле. Однако Stream a является коиндуктивным типом, моделирующим бесконечный список. Он определяется как (точнее, определение эквивалентно) codata Stream a = a :: (Stream a). Невозможно создать бесконечный Список или конечный поток. Однако, когда я пишу определение

codata HList : Type -> Type where
    Nil : HList a
    Cons : a -> HList a -> HList a

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

Итак, позвольте мне сварить их до нескольких основных вопросов:

Разве Haskell не проводит различия между индуктивными и коиндуктивными типами? Если да, то для чего это формализация? Если нет, то что [a]?
Является ли HList коиндуктивным? Если да, то как коиндуктивный тип может содержать конечные значения?
А если мы определили data HList' a = L (List a) | R (Stream a)? Что бы это было рассмотрено и/или было бы полезно для всего HList?

Ответ 1

Из-за лени типы Haskell являются как индуктивными, так и коиндуктивными, или нет формального различия между данными и кодами. Все рекурсивные типы могут содержать бесконечное вложение конструкторов. В таких языках, как Idris, Coq, Agda и т.д. Определение, подобное ones = 1 : ones, отклоняется с помощью проверки завершения. Лень означает, что ones можно оценить за один шаг до 1 : ones, тогда как другие языки оцениваются только в нормальной форме, а ones не имеет нормальной формы.
"Coinductive" не означает "обязательно бесконечный", это означает "определяемый тем, как он деконструирован", если индуктивные средства "определяются тем, как они построены". Я думаю, это является отличным объяснением тонкой разницы. Конечно, вы согласитесь, что тип

codata A : Type where MkA : A

не может быть бесконечным.
Это интересное - в отличие от HList, которое вы никогда не сможете "знать", если оно конечное или бесконечное (в частности, вы можете обнаружить за конечное время, если список конечен, но вы можете 't вычислить, что он бесконечен), HList' дает вам простой способ решить в течение постоянного времени, если ваш список конечен или бесконечен.

Ответ 2

В общем языке, таком как Coq или Agda, индуктивными типами являются те, чьи значения можно снести за конечное время. Индуктивные функции должны заканчиваться. С другой стороны, коиндуктивные типы - это те, чьи ценности могут быть созданы за конечное время. Коиндуктивные функции должны быть продуктивными.

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

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

filter : {A : Set} -> (A -> Bool) -> Stream A -> Stream A
filter f xs with f (head xs)
... | true = head xs :: filter f (tail xs)
... | false = filter f (tail xs)  -- unguarded recursion

Теперь у Хаскелла нет понятия индуктивных или коиндуктивных типов. Вопрос: "Является ли этот тип индуктивным или коиндуктивным?" не имеет смысла. Как Хаскелл уходит, не делая различия? Ну, Хаскелл никогда не собирался быть последовательным как логика в первую очередь. Это частичный язык, а это означает, что вам разрешено писать неограничивающие и непроизводительные функции - нет проверки завершения и без проверки производительности. Можно обсуждать мудрость этого дизайнерского решения, но это, безусловно, делает излишним индукцию и coinduction.

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

Ответ 3

Чтобы интерпретировать рекурсию на уровне типа, нужно найти "фиксированную точку" для CPO-значный функтор списка

F X = (1 + A_bot * X)_bot

Если мы рассуждаем индуктивно, мы хотим, чтобы фиксированная точка была "наименее". Если коиндуктивно, "наибольшее".

Технически это делается путем работы в подкатегории встраивания-проекции CPO_bot, принимая, например, для "наименьшего" столбца диаграммы вложений

0_bot |-> F 0_bot |-> F (F 0_bot) |-> ...

обобщая теорему Клейн о неподвижной точке. Для "наибольшего" мы взяли бы предел диаграммы проекций

0_bot <-| F 0_bot <-| F (F 0_bot) <-| ...

Однако оказывается, что "наименьшее" изоморфно "наибольшему" для любого F. Это теорема "bilimit" (см., Например, обзорную статью "Теория домена" Абрамского).

Возможно, неожиданно получается, что индуктивный или коиндуктивный аромат исходит из поднятий, применяемых F вместо наименьших/наибольших неподвижных точек. Например, если x - разбитое произведение, а # - разбитая сумма,

F X = 1_bot # (A_bot x X)

имел бы как билимит множество конечных списков (до iso).

[Надеюсь, что я правильно понял, это сложно:-)]