Tipo de dato algebraico
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.La construcción correspondiente en los lenguajes de programación se llama Tipo de dato abstracto Sus reglas de tipo polimórficas fueron introducidas por Robin Milner junto con la definición del lenguaje Standard ML y han sido adoptadas desde entonces en diversos lenguajes de programación, sobre todo en los 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: y en sintaxis de Haskell (con información en los nodos de tipo t): Los constructores del tipo Árbol son AVacio y Nodo los cuales, al recibir los argumentos necesarios producen un valor del tipo árbol.Las operaciones sobre los tipos recursivos generalmente se escriben utilizando la construcción de llamada por patrones.En el caso de los árboles éstos son los siguientes: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.