Tipo de datos recursivo

Los tipos de datos también pueden definirse mediante recursión mutua . El ejemplo básico más importante de esto es un árbol , que puede definirse de forma recursiva mutua en términos de un bosque (una lista de árboles). Simbólicamente:

f: [t[1], ..., t[k]] t: vf

Un bosque f consiste en una lista de árboles, mientras que un árbol t consiste en un par formado por un valor v y un bosque f (sus descendientes). Esta definición es elegante y fácil de usar de forma abstracta (por ejemplo, al demostrar teoremas sobre propiedades de árboles), ya que expresa un árbol en términos sencillos: una lista de un tipo y un par de dos tipos.

Esta definición mutuamente recursiva se puede convertir en una definición recursiva simple insertando en línea la definición de un bosque:

t: v [t[1], ..., t[k]]

Un árbol t consta de un par formado por un valor v y una lista de árboles (sus hijos). Esta definición es más compacta, pero algo más compleja: un árbol consta de un par de un tipo y una lista de otro, que requieren ser desentrañados para demostrar resultados sobre él.

En Standard ML , los tipos de datos de árbol y bosque se pueden definir recursivamente de forma mutua como sigue, permitiendo árboles vacíos: ^{[ 1 ]}

tipo de datos 'un árbol = Vacío | Nodo de 'un * 'un bosque y 'un bosque = Nulo | Cons de 'un árbol * 'un bosque

En Haskell, los tipos de datos de árbol y bosque se pueden definir de forma similar:

Árbol de datos a = Vacío | Nodo ( a , Bosque a )Datos Bosque a = Nulo | Cons ( Árbol a ) ( Bosque a )

Con los tipos isorrecursivos, el tipo recursivo${\displaystyle \mu \alpha .T}$y su expansión (o despliegue )${\displaystyle T[\mu \alpha .T/\alpha ]}$(donde la notación${\displaystyle X[Y/Z]}$indica que todas las instancias de Z se reemplazan con Y en X) son tipos distintos (y disjuntos) con construcciones de términos especiales, generalmente llamadas roll y unroll , que forman un isomorfismo entre ellos. Para ser precisos:${\displaystyle roll:T[\mu \alpha .T/\alpha ]\to \mu \alpha .T}$y${\displaystyle unroll:\mu \alpha .T\to T[\mu \alpha .T/\alpha ]}$y estas dos son funciones inversas .

Bajo reglas equirrecursivas, un tipo recursivo${\displaystyle \mu \alpha .T}$y su desarrollo${\displaystyle T[\mu \alpha .T/\alpha ]}$son iguales ; es decir, se entiende que esas dos expresiones de tipo denotan el mismo tipo. De hecho, la mayoría de las teorías de tipos equirrecursivos van más allá y especifican esencialmente que dos expresiones de tipo cualesquiera con la misma "expansión infinita" son equivalentes. Como resultado de estas reglas, los tipos equirrecursivos contribuyen significativamente más a la complejidad de un sistema de tipos que los tipos isorecursivos. Los problemas algorítmicos, como la verificación de tipos y la inferencia de tipos, también son más difíciles para los tipos equirrecursivos. Dado que la comparación directa no tiene sentido en un tipo equirrecursivo, estos pueden convertirse a una forma canónica en tiempo O(n log n), que puede compararse fácilmente. ^{[ 2 ]}

Los tipos isorrecursivos capturan la forma de las definiciones de tipos autorreferenciales (o mutuamente referenciales) que se observan en los lenguajes de programación orientados a objetos nominales , y también surgen en la semántica de la teoría de tipos de objetos y clases . En los lenguajes de programación funcional, los tipos isorrecursivos (bajo la apariencia de tipos de datos) también son comunes. ^{[ 3 ]}