Tipo Co-Inductivo

Un tipo co-inductivo es el opuesto a un tipo inductivo, se define por sus destructores. En este caso podemos usar la \(F\)-co-álgebra de un funtor para representarlo.

Stream

1
2

     (head △ tail)
S.A ───────────────→ A × S.A

Como caso único se puede observar cualquier stream: la cabeza devuelve el primer elemento (head) y la cola devuelve el stream restante (tail). No hay caso base — un stream es siempre infinito.

Co-lista

1
2

      (_• ▽ (head △ tail)) ◦ (=[])?  
L.A ──────────────────────────────────→ 1 + A × L.A

El guard (=[])? decide el camino: si la lista es vacía inyecta _• en el 1 izquierdo; si no, aplica el split (head △ tail) y devuelve A × L.A. Equivale a una lista potencialmente infinita.

Co-árbol binario

1
2

      (val ▽ (left △ right)) ◦ isLeaf?  
T.A ──────────────────────────────────────→ A + T.A × T.A

El guard isLeaf? decide el camino: si es hoja aplica val y devuelve el A izquierdo; si es fork aplica el split (left △ right) y devuelve T.A × T.A. Equivale a un árbol binario potencialmente infinito.