¿Cómo prefiere la lista el señor? Equirrecursiva o isorrecursiva

Supongamos que tenemos un constructor tipos producto (el tipo de los pares ordenados) y un tipo suma (el tipo de un valor opcional entre dos). Entonces, una lista de enteros sería algo como

[$$ List = Empty + ( Integer \times List ) $$]

Una lista es o bien un valor de lista vacía o bien un entero y el resto de la lista. Ahora bien, ¿qué tipo cumple la ecuación anterior? Sencillamente, ninguno. Esto es así porque si sólo tenemos los constructores de tipos producto y suma. Hagamos lo que hagamos, jamás vamos a satisfacer la ecuación de arriba.

Equirrecursividad

La equirecursividad consiste en modificar el modelo en el cual se comprueba la ecuación. Esto viene a ser una modificación del significado de igualdad, de ahí el nombre.

La ecuación de arriba no se puede satisfacer porque sólo podemos usar tipos finitos (usamos el universo de Herbrand). Sea lo que sea el tipo List, al agregarle 

[$$ Empty + ( Integer \times ... ) $$]

al alrededor, hemos generado un tipo distinto.

[$$ List \ne Empty + ( Integer \times List ) $$]

La idea es permitir tipos infinitos (usamos el universo de árboles regulares) de manera que, al tener una extensión infinita, añadir o quitar el contexto

[$$ Empty + ( Integer \times ... ) $$]

del tipo, el resultado sea el mismo.

[$$ List $$]
[$$ = Empty + ( Integer \times ( Empty + ( Integer \times ( Empty + ... ) ) ) ) ) $$]
[$$ = Empty + ( Integer \times List ) $$]

La equirrecursividad permite definir listas, pero este cambio de modelo permite que ciertas expresiones tengan tipo aunque sean algo extrañas.

[$$ \lambda x. x x\ :\ \forall Y. (\mu X. X \rightarrow Y) \rightarrow Y $$]

Una solución es controlar cuándo introducimos o quitamos el contexto

[$$ Empty + ( Integer \times ... ) $$]

Isorecursividad

Volvemos a prohibir que la ecuación

[$$ List = Empty + ( Integer \times List ) $$]

tenga solución. Es decir, volvemos al universo de Herbrand.

Pero lo que vamos a hacer es introducir un isomorfismo entre los tipos de manera que el tipo List sea isomorfo al tipo

[$$ Empty + ( Integer \times List ) $$]

Esto lo escribimos como

[$$ List \equiv\ Empty + ( Integer \times List ) $$]

Ahora tenemos que introducir los isomorfismos. Estos los vamos a llamar fold y unfold. Son funciones que sólo modifican el tipo, no el valor. En este aspecto serían funciones identidad con un tipado especial.

[$$ fold\ :\ Empty + ( Integer \times List ) \rightarrow List $$]
[$$ unfold\ :\ List \rightarrow Empty + ( Integer \times List ) $$]

Afortunadamente estas funciones bastan aplicarlas cuando construimos o destruimos un valor de tipo List. Si tengo el constructor de valores del tipo suma

[$$ inj_l\ empty\ :\ Empty + ( Integer \times List ) $$]

tras aplicarle fold tendríamos

[$$ fold\ inj_l\ empty\ :\ List $$]

He construido una lista. Para destruirla primero hay que usar unfold.

[$$ case\ (unfold l)\ (\lambda .\ ...caso\ Empty...) (\lambda v. ...caso \times ...) $$]

El hecho de que los tipos isorrecursivos usen los isomorfismos fold/unfold justo en la construcción y destrucción ha provocado que se desarrollen los tipos algebraicos (ADT) que aúnan ambos tipos de funciones en una. Pero eso ya es otra historia.