递归数据类型

在计算机编程语言中，递归数据类型（也被称为递归定义、归纳定义或归纳数据类型）是一种用于可能包含相同类型的其他值的数据类型。递归类型的数据通常被看作是有向图。递归在计算机科学中的一个重要应用是定义动态数据结构，如Lists和Trees。递归数据结构可以根据运行时的要求动态地增长到一个任意大的尺寸；相反，静态数组的尺寸要求必须在编译时设置。有时，术语归纳数据类型被用于不一定是递归的代数数据类型。

一个例子是Haskell中的列表类型。dataLista=Nil|Consa(Lista)这表明一个a的列表要么是一个空列表，要么是一个包含一个'a'（列表的头）和另一个列表（尾）的cons单元。另一个例子是Java中类似的单链类型。这表明E类型的非空列表包含一个E类型的数据成员，以及对列表其余部分的另一个List对象的引用（或者一个空引用以表明这是列表的结束）。

数据类型也可以通过相互递归来定义。这方面最重要的基本例子是树，它可以用森林（一个树的列表）来相互递归地定义。用符号表示。f:[t[1],...,t[k]]t:vf一个森林f由一个树的列表组成，而一棵树t由一对值v和一个森林f（其子）组成。这个定义很优雅，而且很容易抽象地使用（比如在证明关于树的属性的定理时），因为它用简单的术语表达了一棵树：一个类型的列表和两个类型的一对。这个相互递归的定义可以通过内联森林的定义转换为单一递归的定义。一个树t由一对值v和一个树（其子）的列表组成。这个定义更紧凑，但也更混乱：一棵树由一个类型的对和一个列表的对组成，这需要分解来证明有关结果。在标准ML中，树和森林数据类型可以相互递归定义如下，允许空树。数据类型'atree=Empty|Nodeof'a*'aforestand'aforest=Nil|Consof'atree*'aforest在Haskell中，树和森林的数据类型可以被类似地定义。

在类型理论中，递归类型的一般形式是μα.T，其中类型变量α可能出现在类型T中，代表整个类型本身。例如，自然数（见Peano算术）可以由Haskell数据类型定义。其中，和类型的两个臂膀代表Zero和Succ数据构造函数。Zero不需要参数（因此用单位类型表示），Succ需要另一个Nat（因此是另一个元素的递归类型有两种形式：所谓的等距递归类型，以及等距递归类型。这两种形式的区别在于递归类型的项是如何被引入和消除的。

对于等距递归类型，递归类型表示Z的所有实例在X中被替换为Y）是不同的（且不相交的）类型，具有特殊的术语构造，通常称为roll和unroll，它们之间形成了同构。准确地说，是{displaystyleunroll:'mualpha.TtoT[mualpha.T/alpha]}，这两个是反函数。，而这两个是反函数。等价递归类型在等价递归规则下，一个递归类型是相等的--也就是说，这两个类型表达式被理解为表示同一类型。事实上，大多数等距类型的理论更进一步，基本上规定任何两个具有相同的无限扩展的类型表达式是等价的。由于这些规则，等价递归类型对类型系统的复杂性的贡献比等价递归类型大得多。算法问题，如类型检查和类型推理，对等价递归类型来说也更加困难。由于直接比较在等价cursive类型上是没有意义的，它们可以在O(nlogn)时间内被转换为典型形式，这可以很容易地实现