这只是部分答案。
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
在哈斯克尔是。这有一定道理。类似地,归纳情况必须是多态函数,就像Cons
是。还有一个额外的List2 a
争论,但如果我们愿意的话,我们可以忽略它。
现在,上面仍然是一种折叠/猫regular类型。那么非常规的呢?我会学习
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
用哈斯克尔表示法:
(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 代数......;-)