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
然而，对我来说不清楚的是，如果使用相同的类型构造函数，但是使用不同的类型参数会发生什么。例如。而不是将列表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 – >列表b – > b)，即仅替换所有列出应用程序。
哪两个是正确的，为什么？还是不一样呢？
OP提出的问题是：如果在非常规递归类型的情况下如何定义fold / cata？
既然我不相信自己这个权利，我会诉诸于要求Coq。我们从一个简单的，常规的递归列表类型开始。
Inductive List (A : Type) : Type := | Empty: List A | Cons : A -> List A -> List A .
在这里没有什么想法，列表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列表是常数类型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
哪个是折叠，除了“当前列表”也传递给二进制函数参数 – 不是主要区别。
现在，在Coq中，我们可以用另一种微妙的方式定义一个列表：
Inductive List2 : Type -> Type := | Empty2: forall A,List2 A | Cons2 : forall A,A -> List2 A -> List2 A .
它看起来是一样的，但是有一个深刻的区别。这里我们没有按照List A定义类型List A.而是我们定义一个类型函数List2：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
我们像以前一样从P中删除List2 T参数，基本上假定P是恒定的。
forall P : forall T : Type,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),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
不错 – 基本情况现在必须是一个多态函数，就像Haskell中的空格一样。这有道理类似地，归纳情况必须是多态函数，就像缺点一样。有一个额外的List2一个参数，但是我们可以忽略，如果我们想要的话。
现在，上面的一种是常规类型的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,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),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代数…
