Являются ли списки индуктивными или индуктивными в Хаскеле?

Question

Так что в последнее время я читаю о коиндукции, и теперь мне интересно: списки на 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, а именно то, что я могу создавать как конечные, так и бесконечные структуры.

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

1. Разве Хаскелл не различает индуктивный и коиндуктивный типы? Если так, что формализация для этого? Если нет, то что [а]?

2. Является ли HList коиндуктивным? Если это так, как коиндуктивный тип может содержать конечные значения?

3. Что если мы определили data HList' a = L (List a) | R (Stream a)? Что это будет считаться и / или будет ли полезно в течение всего HList?

Answer 1

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

2. "Коиндуктивный" не означает "обязательно бесконечный", он означает "определенный по тому, как он деконструирован", тогда как индуктивный означает "определенный по тому, как он построен". Я думаю, что это отличное объяснение тонкой разницы. Конечно, вы бы согласились, что тип

   codata A : Type where MkA : A

   не может быть бесконечным.

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

Answer 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

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

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

Answer 3

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

F X = (1 + A_bot * X)_bot

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

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

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

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

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

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

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

F X = 1_bot # (A_bot x X)

будет иметь в качестве bilimit множество конечных списков (до ISO).

[Надеюсь, я правильно выбрал лифтинг - это сложно;-) ]