对于非常规递归类型,catamorphism(fold)的类型是什么？

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-algebras ... ;-)