Каков тип катаморфизма (складки) для нерегулярных рекурсивных типов?

Question

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

data Bool = False | True 
foldBool :: r    -- False constructor 
     -> r    -- True constructor 
     -> Bool -> r 

data Maybe a = Nothing | Just a 
foldMaybe :: b    -- Nothing constructor 
      -> (a -> b)  -- Just constructor 
      -> Maybe a -> b 

data List a = Empty | Cons a (List a) 
foldList :: b    -- Empty constructor 
     -> (a -> b -> b) -- Cons constructor 
     -> List a -> b 

Однако, что мне не понятно, что происходит, если используется тот же конструктор типа, но с другим типом аргумента. Например. вместо передачи List a к Cons, что о

data List a = Empty | Cons a (List (a,a)) 

Или, может быть, более сумасшедший случай:

data List a = Empty | Cons a (List (List a)) 
foldList :: b    -- Empty constructor 
     -> ???   -- Cons constructor 
     -> List a -> b 

Две правдоподобные идеи у меня есть для ??? части являются

• (a -> b -> b) , т.е. рекурсивно заменяя все применения конструктора List)
• (a -> List b -> b), т. Е. Просто заменить все приложения List a.

Какой из двух будет правильным - и почему? Или это совсем другое?

Answer 1

Это частичный ответ, только.

Проблема, которую поднимает ОП: как определить fold/cata в случае нерегулярных рекурсивных типов?

Поскольку я не верю себе в этом, я прибегну к просьбе Кока. Начнем с простого, регулярного рекурсивного типа списка.

Inductive List (A : Type) : Type := 
    | Empty: List A 
    | Cons : A -> List A -> List A 
. 

Ничего особенного здесь, List A определяется в терминах List A. (Помните об этом - мы вернемся к этому.)

Как насчет cata? Давайте обратимся к индукционному ключу.

> Check List_rect. 
forall (A : Type) (P : List A -> Type), 
    P (Empty A) -> 
    (forall (a : A) (l : List A), P l -> P (Cons A a l)) -> 
    forall l : List A, P l 

Давайте посмотрим. Вышеперечисленные типы зависимых типов: P зависит от фактического значения списка. Давайте просто упростим его вручную в случае P list является постоянным типом B. Получаем:

forall (A : Type) (B : Type), 
    B -> 
    (forall (a : A) (l : List A), B -> B) -> 
    forall l : List A, B 

, который может быть эквивалентно записать в виде

forall (A : Type) (B : Type), 
    B -> 
    (A -> List A -> B -> B) -> 
    List A -> B 

Который является foldr исключением того, что «текущий список» также передается в двоичном аргумент функции - не большая разница.

Теперь в Coq мы можем определить список в другой тонко иначе:

Inductive List2 : Type -> Type := 
    | Empty2: forall A, List2 A 
    | Cons2 : forall A, A -> List2 A -> List2 A 
. 

Он выглядит тот же тип, но есть глубокая разница. Здесь мы не определяем тип List A в терминах List A.Скорее, мы определяем функцию типа List2 : Type -> Type в терминах List2. Главное, что рекурсивные ссылки на List2 не должны применяться к A - тот факт, что выше мы делаем это, является только инцидентом.

Во всяком случае, давайте посмотрим на тип для индукционного принципа:

> Check List2_rect. 
forall P : forall T : Type, List2 T -> Type, 
    (forall A : Type, P A (Empty2 A)) -> 
    (forall (A : Type) (a : A) (l : List2 A), P A l -> P A (Cons2 A a l)) -> 
    forall (T : Type) (l : List2 T), P T l 

Давайте удалим List2 T аргумент из P, как мы делали раньше, в основном при условии P постоянна на ней.

forall P : forall T : Type, Type, 
    (forall A : Type, P A) -> 
    (forall (A : Type) (a : A) (l : List2 A), P A -> P A) -> 
    forall (T : Type) (l : List2 T), P T 

Эквивалентное переписано:

forall P : (Type -> Type), 
    (forall A : Type, P A) -> 
    (forall (A : Type), A -> List2 A -> P A -> P A) -> 
    forall (T : Type), List2 T -> P T 

что примерно соответствует, в Haskell нотации

(forall a, p a) ->       -- Empty 
(forall a, a -> List2 a -> p a -> p a) -> -- Cons 
List2 t -> p t 

Не так уж плохо - базовый вариант теперь должен быть полиморфной функции, так же как Empty в Haskell. Это имеет смысл. Точно так же индуктивный случай должен быть полиморфной функцией, так же как Cons. Есть дополнительный аргумент List2 a, но мы можем игнорировать это, если хотим.

Теперь вышесказанное по-прежнему является разновидностью складок/катанов на обычных типа. А как насчет нерегулярных? Я буду изучать

data List a = Empty | Cons a (List (a,a)) 

который в Coq становится:

Inductive List3 : Type -> Type := 
    | Empty3: forall A, List3 A 
    | Cons3 : forall A, A -> List3 (A * A) -> List3 A 
. 

с индукционным принципом:

> Check List3_rect. 
forall P : forall T : Type, List3 T -> Type, 
    (forall A : Type, P A (Empty3 A)) -> 
    (forall (A : Type) (a : A) (l : List3 (A * A)), P (A * A) l -> P A (Cons3 A a l)) -> 
    forall (T : Type) (l : List3 T), P T l 

Отсоединение "зависимый" часть:

forall P : (Type -> Type), 
    (forall A : Type, P A) -> 
    (forall (A : Type), A -> List3 (A * A) -> P (A * A) -> P A) -> 
    forall (T : Type), List3 T -> P T 

В Haskell нотации :

(forall a. p a) ->          -- empty 
    (forall a, a -> List3 (a, a) -> p (a, a) -> p a) -> -- cons 
    List3 t -> p t 

Помимо дополнительного аргумента List3 (a, a), это своего рода складка.

И наконец, как насчет типа OP?

data List a = Empty | Cons a (List (List a)) 

Увы, Кок не принимает тип

Inductive List4 : Type -> Type := 
    | Empty4: forall A, List4 A 
    | Cons4 : forall A, A -> List4 (List4 A) -> List4 A 
. 

поскольку внутренний List4 возникновение не в строго положительной позиции. Вероятно, это намек на то, что я должен перестать быть ленивым и использовать Coq для выполнения этой работы, и сам подумаю о задействованных F-алгебрах ... ;-)