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

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

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.

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

Ответ 1

Это частичный ответ.

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

Так как я не верю себе в этом, я прибегну к просьбе вместо Coq. Давайте начнем с простого, регулярного рекурсивного типа списка.

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, но мы можем игнорировать это, если хотим.

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

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))

Увы, Coq не принимает тип

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

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