haskell - 非常规递归类型的变态(折叠)类型是什么？

Question

许多 catamorphisms 似乎很简单，主要是用自定义函数替换每个数据构造函数，例如

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

这只是部分答案。

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争论，但如果我们愿意，我们可以忽略它。

现在，以上仍然是常规类型上的一种折叠/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 代数...... ;-)