Tipo de datos algebraicos

En programación informática , especialmente en programación funcional y teoría de tipos , un tipo de dato algebraico ( TDA ) es un tipo de dato compuesto , es decir, un tipo formado mediante la combinación de otros tipos.

Un tipo de dato algebraico se define mediante dos construcciones clave: una suma y un producto . A veces se les denomina tipos "OR" y "AND".

Un tipo suma es una elección entre posibilidades. El valor de un tipo suma puede coincidir con una de varias variantes definidas . Por ejemplo, un tipo que representa el estado de un semáforo podría ser Red, Amber, o Green. Un tipo forma podría ser Circle(que almacena un radio) o ( Squareque almacena un ancho). En términos formales, estas variantes se conocen como uniones etiquetadas o uniones disjuntas . Cada variante tiene un nombre, llamado constructor , que también puede contener datos. Los tipos enumerados son una forma simple de tipo suma donde los constructores no contienen datos.

Un tipo de producto combina varios tipos. Un valor de un tipo de producto contiene un valor para cada uno de sus tipos componentes. Por ejemplo, un Pointtipo podría definirse para contener una xcoordenada (un entero) y otra ycoordenada (también un entero). Ejemplos formales de tipos de producto incluyen tuplas y registros . El conjunto de todos los valores posibles de un tipo de producto es el producto cartesiano de los conjuntos de sus tipos componentes.

Los valores de tipos de datos algebraicos se manejan normalmente mediante la coincidencia de patrones . Esta característica permite al programador comprobar con qué constructor se creó un valor y extraer los datos que contiene de forma práctica y segura en cuanto a tipos.

Los tipos de datos algebraicos se introdujeron en Hope , un pequeño lenguaje de programación funcional desarrollado en la década de 1970 en la Universidad de Edimburgo . ^{[ 1 ]}

Los tipos de datos algebraicos se utilizan para representar valores que pueden ser de varios tipos . Cada tipo de dato se asocia con un identificador llamado constructor , que puede considerarse una etiqueta para ese tipo de datos. Cada constructor puede contener un tipo de dato diferente.

Por ejemplo, considerando el Treeejemplo binario mostrado anteriormente, un constructor podría no contener datos (por ejemplo, Empty), o un dato (por ejemplo, Leaftiene un valor Int), o varios datos (por ejemplo, Nodetiene un Intvalor y dos Treevalores).

Para trabajar con un valor de este Treetipo de dato algebraico, se descompone mediante un proceso llamado coincidencia de patrones . Esto implica comparar los datos con una serie de patrones . La función de ejemplo depthanterior compara su argumento con tres patrones. Al llamar a la función, encuentra el primer patrón que coincide con su argumento, realiza las asignaciones de variables que se encuentran en el patrón y evalúa la expresión correspondiente.

Cada patrón anterior tiene una forma que se asemeja a la estructura de algún valor posible de este tipo de dato. El primer patrón simplemente coincide con los valores del constructor Empty. El segundo patrón coincide con los valores del constructor Leaf. Los patrones son recursivos, por lo que los datos asociados con ese constructor coinciden con el patrón "n". En este caso, un identificador en minúscula representa un patrón que coincide con cualquier valor, el cual luego se vincula a una variable con ese nombre; en este caso, una variable " n" se vincula al valor entero almacenado en el tipo de dato, para ser utilizado en la expresión a evaluar.

La recursión en los patrones de este ejemplo es trivial, pero un posible patrón recursivo más complejo sería algo como:

Nodei(Nodej(Leaf4)x)(Nodeky(NodeEmptyz))

Los patrones recursivos de varias capas de profundidad se utilizan, por ejemplo, para equilibrar árboles rojo-negro , que implican casos que requieren examinar colores de varias capas de profundidad.

El ejemplo anterior es operacionalmente equivalente al siguiente pseudocódigo :

switch on ( data . constructor ) case Empty : return 0 case Leaf : let n = data . field1 return 1 case Node : let l = data . field2 let r = data . field3 return 1 + max ( depth l ) ( depth r )

Las ventajas de los tipos de datos algebraicos se pueden destacar comparando el pseudocódigo anterior con un equivalente de coincidencia de patrones.

En primer lugar, está la seguridad de tipos . En el ejemplo de pseudocódigo anterior, se requiere diligencia del programador para no accedercampo2Cuando el constructor es de tipo Leaf. El sistema de tipos tendría dificultades para asignar un tipo estático de forma segura para las estructuras de datos de registro tradicionales . Sin embargo, en la coincidencia de patrones no se presentan tales problemas. El tipo de cada valor extraído se basa en los tipos declarados por el constructor correspondiente. La cantidad de valores que se pueden extraer se conoce según el constructor.

En segundo lugar, en la coincidencia de patrones, el compilador realiza una comprobación exhaustiva para asegurar que se contemplen todos los casos. Si faltara alguno de los casos de la función de profundidad anterior, el compilador emitiría una advertencia. La comprobación exhaustiva puede parecer sencilla para patrones simples, pero con muchos patrones recursivos complejos, la tarea pronto se vuelve difícil para el usuario promedio (o para el compilador, si debe comprobar construcciones condicionales anidadas arbitrarias). Del mismo modo, puede haber patrones que nunca coincidan (es decir, que ya estén cubiertos por patrones anteriores). El compilador también puede comprobarlos y emitir advertencias, ya que pueden indicar un error de razonamiento.

La coincidencia de patrones en tipos de datos algebraicos no debe confundirse con la coincidencia de patrones en cadenas de expresiones regulares . Si bien el objetivo de ambas es similar (extraer partes de un conjunto de datos que cumplan ciertas restricciones), su implementación es muy diferente. La coincidencia de patrones en tipos de datos algebraicos se basa en las propiedades estructurales de un objeto, en lugar de en la secuencia de caracteres de las cadenas.

Un tipo de dato algebraico general es un tipo de suma posiblemente recursivo de tipos de producto . Cada constructor etiqueta un tipo de producto para separarlo de los demás, o si solo hay un constructor, el tipo de dato es un tipo de producto. Además, los tipos de parámetros de un constructor son los factores del tipo de producto. Un constructor sin parámetros corresponde al producto vacío . Si un tipo de dato es recursivo, la suma completa de productos se encapsula en un tipo recursivo , y cada constructor también incorpora el tipo de dato al tipo recursivo.

Por ejemplo, el tipo de dato de Haskell:

Lista de datos a = Nil | Cons a ( Lista a )

se representa en la teoría de tipos como ${\displaystyle \lambda \alpha .\mu \beta .1+\alpha \times \beta }$ con constructores${\displaystyle \mathrm {nil} _{\alpha }=\mathrm {roll} \ (\mathrm {inl} \ \langle \rangle )}$y${\displaystyle \mathrm {cons} _{\alpha }\ x\ l=\mathrm {roll} \ (\mathrm {inr} \ \langle x,l\rangle )}$.

El tipo de dato Lista de Haskell también puede representarse en la teoría de tipos de una forma ligeramente diferente, de la siguiente manera: ${\displaystyle \mu \phi .\lambda \alpha .1+\alpha \times \phi \ \alpha }$. (Observe cómo el${\displaystyle \mu }$y${\displaystyle \lambda }$Las construcciones se invierten con respecto a la original.) La formación original especificaba una función de tipo cuyo cuerpo era un tipo recursivo. La versión revisada especifica una función recursiva sobre tipos. (La variable de tipo${\displaystyle \phi }$se utiliza para sugerir una función en lugar de un tipo base como${\displaystyle \beta }$, desde${\displaystyle \phi }$es como una f griega .) Ahora también se debe aplicar la función.${\displaystyle \phi }$a su tipo de argumento${\displaystyle \alpha }$en el cuerpo del tipo.

Para el ejemplo de la lista, estas dos formulaciones no difieren significativamente; sin embargo, la segunda permite expresar los llamados tipos de datos anidados , es decir, aquellos en los que el tipo recursivo difiere paramétricamente del original. (Para más información sobre tipos de datos anidados, véanse las obras de Richard Bird , Lambert Meertens y Ross Paterson).

En teoría de conjuntos, el equivalente de un tipo suma es una unión disjunta , un conjunto cuyos elementos son pares que consisten en una etiqueta (equivalente a un constructor) y un objeto de un tipo que corresponde a la etiqueta (equivalente a los argumentos del constructor). ^{[ 2 ]}

Muchos lenguajes de programación incorporan tipos de datos algebraicos como una noción de primera clase, entre ellos:

• Unión disjunta
• Tipo de datos algebraicos generalizados
• Álgebra inicial
• Tipo de cociente
• Unión etiquetada
• teoría de tipos
• Patrón de visitantes