Tipo inductivo

Un tipo inductivo es un tipo de dato construido por constructores. Así se definen por un caso base y un caso inductivo.
Podemos usar la \(F\)-álgebra de un funtor para representar la construcción de estos tipos.

Naturales

1
2

   (0• ▽ 1+)
N ←────────── 1+N

Como caso base se añade el 0 y como caso inductivo se suma 1 las veces que haga falta.

Listas

1
2

     ([]• ▽ ⊢)
L.A ←───────────── 1+AxL.A

Como caso base se toma la lista vacía y como caso inductivo se concadena cualquier elemento de A con cualquier lista ya generada.

Árboles

1
2

     (L ▽ ⋔)
T.A ←───────────── A+T.AxT.A

Como caso base se toma únicamente un elemento de A (transformado a árbol por la función Leaf) como hoja del árbol, como caso inductivo se junta cualquier par de árboles ya generado para crear uno más alto.