Ver el código de «Tipo de dato algebraico»

En [[matemática discreta|matemáticas discretas]] es usual introducir definiciones de estructuras recursivas dando los casos de definición y un axioma de clausura indicando que ninguna otra cosa forma parte de lo definido.

Por ejemplo, los árboles con información en los nodos pueden definirse como sigue:

Sea ''T'' un conjunto. Los árboles con información en los nodos son todos los valores que se pueden construir con las reglas siguientes.
# El árbol vacío es un árbol y es representado con la constante ''AVacio''.
# Si <math>t_1</math> y <math>t_2</math> son árboles, y ''x'' es un elemento de ''T'', entonces ''Nodo(<math>t_1</math>,x,<math>t_2</math>)'' es un árbol.
# Los árboles son únicamente los valores que se construyen utilizando las reglas 1 y 2.

La construcción correspondiente en los [[lenguaje de programación|lenguajes de programación]] se llama ''[[Tipo de dato abstracto]]'' Sus [[análisis de tipos|reglas de tipo]] [[Polimorfismo (programación orientada a objetos)|polimórficas]] fueron introducidas por [[Robin Milner]] junto con la definición del lenguaje [[Lenguaje de programación Standard ML|Standard ML]] y han sido adoptadas desde entonces en diversos lenguajes de programación, sobre todo en los [[Programación funcional|lenguajes de programación funcionales]]. Por ejemplo, la definición del tipo [[árbol binario]] con información en los nodos de tipo ''T'' se escribe en [[OCaml]] como sigue:
<syntaxhighlight lang="haskell">
 type 'T Arbol = AVacio | Nodo of ('T Arbol * 'T * 'T Arbol)
</syntaxhighlight>
y en sintaxis de [[Haskell]] (con información en los nodos de tipo ''t''):
<syntaxhighlight lang="haskell">
 data Arbol t = AVacio | Nodo (Arbol t) t (Arbol t)
</syntaxhighlight>
Los constructores del tipo Árbol son ''AVacio'' y ''Nodo'' los cuales,
al recibir los argumentos necesarios producen un valor del tipo
árbol. Por ejemplo, en Ocaml, ''AVacio'' es un árbol al igual que ''Nodo (AVacio,5,AVacio)''. 

Las operaciones sobre los tipos recursivos generalmente se escriben
utilizando la construcción de [[llamada por patrones]]. Por ejemplo,
en Haskell, el número de niveles de un árbol se define como:

<syntaxhighlight lang="haskell">
 niveles :: Arbol t -> Int
 niveles AVacio = 0
 niveles (Nodo i n d) = 1 + max (niveles i) (niveles d)
</syntaxhighlight>
en Standard ML la misma función se escribe

<syntaxhighlight lang="sml">
 fun niveles AVacio = 0
   | niveles Nodo(i,n,d) = 1 + max (niveles i) (niveles d)
</syntaxhighlight>
== Corrección de programas ==
A cada tipo de datos del lenguaje algebraico corresponde el [[orden bien fundamentado]] de subtérminos y un esquema de [[inducción estructural]] sobre la base de la definición del tipo. En el caso de los árboles éstos son los siguientes:

<center>
<math> t_1 < Nodo(t_1,n,t_2)~~~ ~~~t_2 < Nodo(t_1,n,t_2) </math>

<math>\frac{P(AVacio) \wedge (\forall i,n,d:i,d\in Arbol(T): P(i) \wedge P(d) \Rightarrow P(Nodo(i,n,d)))}{(\forall x:x\in Arbol(T):P(x))}</math>
</center>

Para demostrar la terminación de la función niveles aplicando este esquema de inducción
estructural, se tiene que demostrar, utilizando las reglas semánticas del lenguaje, que la expresión ''(niveles AVacio)'' termina y que si ''(niveles i)'' y ''(niveles d)'' terminan entonces ''(niveles (Nodo (i, n, d))'' termina también.

La llamada por patrones es una operación compleja que puede definirse con ayuda de dos primitivas, El operador ''is'' permite identificar el caso particular de una definición y la definición estructurada de variables permite obtener los componentes de un caso ya identificado:

En el ejemplo de árboles, el predicado ''e is AVacio'' es cierto cuando el árbol ''e'' es efectivamente un árbol vacío y ''e is Nodo'' es cierto cuando ''e'' es un nodo. Una definición del tipo ''let Nodo (u, x, v) = e ...'', que sólo tiene sentido cuando ''e is Nodo'' es cierto, permite asociar a las variables ''u, x, v'' los componentes del nodo.

== Enlaces externos ==
* [https://web.archive.org/web/20050414212018/http://wombat.doc.ic.ac.uk/foldoc/foldoc.cgi?algebraic+data+type FOLDOC (Algebraic data type)]
{{Control de autoridades}}
[[Categoría:Tipos de datos|Algebraico]]