非常规递归类型的变形类型（折叠）是什么类型？ [英] What's the type of a catamorphism (fold) for non-regular recursive types?

问题描述

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

  data Bool = False | True 
 foldBool :: r  - 假构造函数
  - > r  - 真正的构造函数
  - >布尔 - > r 
 
 data也许a = Nothing |只需
 foldMaybe :: b  - 无构造函数
  - > （a  - > b） - 只是构造函数
  - >也许是 - > b 
 
数据列表a =空|缺点（列表a）
 foldList :: b  - 空构造函数
  - > （a  - > b  - > b） - 缺点构造函数
  - >列表a  - > b 
  

但是，我不清楚如果使用相同类型的构造函数会发生什么，一个不同类型的参数。例如。而不是传递一个列出一个到缺点，怎么样


 数据列表a =空|缺点a（List（a，a））
  

或者，也许更疯狂的情况：

 数据列表a =空|缺点（List（List a））
 foldList :: b  - 空构造函数
  - > ??? - 缺点构造函数
  - >列表a  - > b 
  

我对 ??? c $ c>部分是




（a - > b - > b），即递归地替换 List 构造函数的所有应用程序）

（a - > List b - > b），即仅替换所有列出一个应用程序。

两者中的哪一个是正确的 - 为什么？或者它会是完全不同的东西？

解决方案

这只是一个部分答案。 b $ b

OP提出的问题是：在非情况下如何定义 fold / cata - 规则递归类型？

因为我不相信自己能够做到这一点，所以我会求助于Coq。我们从一个简单的常规递归列表类型开始。

 归纳列表（A：类型）：类型：= 
 |空：列出A 
 |缺点：A  - >列表A  - >列出A 
。 
  

这里没什么特别的， List A 被定义根据列表A 。
（请记住这一点 - 我们将回到它。）

那么 cata ？让我们来查询感应原理。

 >检查List_rect。 
 forall（A：Type）（P：List A  - > Type），
 P（Empty A） - > 
（forall（a：A）（l：列表A），P l→P（Cons A a l）） - > 
 forall l：列表A，P l 
  

让我们来看看。以上利用依赖类型： P 取决于列表的实际值。在 P列表是一个常量类型 B 的情况下，让我们手动简化它。我们获得：

  forall（A：Type）（B：Type），
 B  - > 
（forall（a：A）（l：列表A），B  - > B） - > 
 forall l：列表A，B 
  

可以等同写成

（A：Type）（B：Type），
B - >

  
（A→> List A→> B→> B）→> 
列表A  - > B 
  

foldr 除了当前列表也传递给二元函数参数 - 并非主要区别。

现在，在Coq中，我们可以用另一种不同的方式定义一个列表： p>

 归纳列表2：类型 - >类型：= 
 | Empty2：Forall A，List2 A 
 | Cons2：Forall A，A  - > List2 A  - > List2 A 
。 
  

它看起来是相同的类型，但有很大的不同。这里我们没有按照 List A 定义类型 List A 。相反，我们正在定义一个类型函数 List2：Type - >按照 List2 键入。其主要意义在于对 List2 的递归引用不一定适用于 A - 事实上面我们这样做只是一个事件。

无论如何，让我们看看归纳原理的类型：

 >检查List2_rect。 
 forall P：forall T：Type，List2 T  - >类型，
（全部A：类型，P A（Empty2 A）） - > （a：Type）（a：A）（l：List2 A），P A l  - > P A（Cons2 A a 1）） - > 
 forall（T：Type）（l：List2 T），PT l 
  

让我们移除与我们之前一样， P 中的 List2 T 参数，基本上假设 P


  forall P：forall T：Type，Type，
（forall A：类型，PA） - > （a：Type）（a：A）（l：List2 A），P A  - > P A） - > 
 forall（T：Type）（l：List2 T），PT 
  

等价改写：

  forall P：（类型 - >类型），
（全部A：类型，PA） - > 
（全部（A：类型），A→>列表2 A→> P A→P A）→> 
 forall（T：Type），List2 T  - > PT 
  

在Haskell符号中大致相应

 （forall a，pa） - > - 空
（全部a，a  - > List2 a  - > p a  - > p a） - > -  Cons 
 List2 t  - > pt 
  

不错 - 基本情况现在必须是一个多态函数，很像<$在Haskell中c $ c> Empty 是。这是有道理的。同样，归纳情况必须是一个多态函数，就像 Cons 一样。还有一个额外的 List2 a 参数，但如果需要，我们可以忽略它。

现在，上面是仍然是常规类型的折叠/加值。那么非常规的呢？我会研究

 数据列表a =空|在Coq中变成：（a（List，a））
  

 归纳列表3：类型 - >类型：= 
 | Empty3：Forall A，List3 A 
 | Cons3：Forall A，A  - > List3（A * A） - > List3 A 
。 
  

带归纳原理：

 >检查List3_rect。 
 forall P：forall T：Type，List3 T  - >类型，
（全部A：类型，P A（Empty3 A）） - > （a：Type）（a：A）（l：List3（A * A）），P（A * A）l→P A（Cons3 A a l）） - > b 
 
 
 
 
 
删除依赖部分：
 
 
  forall P：（Type  - &> Type），
（forall A：Type， PA） - > （A：Type），A  - > List3（A * A） - > P（A * A） - > P A） - > 
 forall（T：Type），List3 T  - > PT 
  
在Haskell记法中：
 
 
 （forall a。pa） - > - 空
（全部a，a  - > List3（a，a） - > p（a，a） - > p a） - > -  cons 
 List3 t  - > pt 
  
除了附加的 List3（a，a） 
 
最后，OP类型怎么样？
 数据列表a =空|缺点（列表（列表a））
  
唉，Coq不接受类型
 归纳式List4：类型 - >类型：= 
 | Empty4：Forall A，List4 A 
 | Cons4：Forall A，A  - > List4（List4 A） - > List4 A 
。 
  
由于内部 List4 发生不在严格肯定的地位。这可能暗示我应该停止懒惰，并使用Coq来完成这项工作，并开始考虑自己涉及的F-代数......;  - ）
 
Many catamorphisms seem to be simple enough, mostly replacing each data constructor with a custom function, e.g.
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
However, what's not clear to me is what happens if the same type constructor is used, but with a different type argument. E.g. instead of passing a List a to Cons, what about
data List a = Empty | Cons a (List (a,a))
Or, maybe a more crazy case:
data List a = Empty | Cons a (List (List a))
foldList :: b              -- Empty constructor
         -> ???            -- Cons constructor
         -> List a -> b
The two plausible ideas I have for the ??? part are


(a -> b -> b), i.e. replacing all applications of the List constructor recursively)
(a -> List b -> b), i.e. merely replacing all List a applications.


Which of the two would be correct - and why? Or would it be something different altogether?
解决方案
This is a partial answer, only.

The issue the OP raises is: how to define fold/cata in the case of non-regular recursive types?

Since I don't trust myself in getting this right, I will resort to asking Coq instead. Let's start from a simple, regular recursive list type.
Inductive List (A : Type) : Type :=
  | Empty: List A
  | Cons : A -> List A -> List A
.
Nothing fancy here, List A is defined in terms of List A.
(Remember this -- we'll get back to it.)

What about the cata? Let's query the induction pinciple.
> 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
Let's see. The above exploits dependent types: P depends on the actual value of the list. Let's just manually simplify it in the case P list is a constant type B. We obtain:
forall (A : Type) (B : Type),
   B ->
   (forall (a : A) (l : List A), B -> B) ->
   forall l : List A, B
which can be equivalently written as
forall (A : Type) (B : Type),
   B ->
   (A -> List A -> B -> B) ->
   List A -> B
Which is foldr except that the "current list" is also passed to the binary function argument -- not a major difference.

Now, in Coq we can define a list in another subtly different way:
Inductive List2 : Type -> Type :=
  | Empty2: forall A, List2 A
  | Cons2 : forall A, A -> List2 A -> List2 A
.
It looks the same type, but there is a profound difference. Here we are not defining the type List A in terms of List A. Rather, we are defining a type function List2 : Type -> Type in terms of List2. The main point of this is that the recursive references to List2 do not have to be applied to A -- the fact that above we do so is only an incident.

Anyway, let's see the type for the induction principle:
> 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
Let's remove the List2 T argument from P as we did before, basically assuming P is constant on it.
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
Equivalently rewritten:
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
Which roughly corresponds, in Haskell notation
(forall a, p a) ->                          -- Empty
(forall a, a -> List2 a -> p a -> p a) ->   -- Cons
List2 t -> p t
Not so bad -- the base case now has to be a polymorphic function, much as Empty in Haskell is. It makes some sense. Similarly, the inductive case must be a polymorphic function, much as Cons is. There's an extra List2 a argument, but we can ignore that, if we want.

Now, the above is still a kind of fold/cata on a regular type. What about non regular ones? I will study
data List a = Empty | Cons a (List (a,a))
which in Coq becomes:
Inductive  List3 : Type -> Type :=
  | Empty3: forall A, List3 A
  | Cons3 : forall A, A -> List3 (A * A) -> List3 A
.
with induction principle:
> 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
Removing the "dependent" part:
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
In Haskell notation:
   (forall a. p a) ->                                      -- empty
   (forall a, a -> List3 (a, a) -> p (a, a) -> p a ) ->    -- cons
   List3 t -> p t
Aside from the additional List3 (a, a) argument, this is a kind of fold.

Finally, what about the OP type?
data List a = Empty | Cons a (List (List a))
Alas, Coq does not accept the type
Inductive  List4 : Type -> Type :=
  | Empty4: forall A, List4 A
  | Cons4 : forall A, A -> List4 (List4 A) -> List4 A
.
since the inner List4 occurrence is not in a strictly positive position. This is probably a hint that I should stop being lazy and using Coq to do the work, and start thinking about the involved F-algebras by myself... ;-)

                        
这篇关于非常规递归类型的变形类型（折叠）是什么类型？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！