tipo de opción
En los lenguajes de programación (especialmente los lenguajes de programación funcionales ) y la teoría de tipos , un tipo de opción o tal vez un tipo es un tipo polimórfico que representa la encapsulación de un valor opcional; por ejemplo, se utiliza como el tipo de devolución de funciones que pueden o no devolver un valor significativo cuando se aplican. Consiste en un constructor que está vacío (a menudo llamado Noneo Nothing), o que encapsula el tipo de datos original A(a menudo escrito Just Ao Some A).
Un concepto distinto, pero relacionado fuera de la programación funcional, que es popular en la programación orientada a objetos , se denomina tipos anulables (a menudo expresados como A?). La principal diferencia entre los tipos de opciones y los tipos que aceptan valores NULL es que los tipos de opciones admiten la anidación ( Maybe (Maybe A)≠ Maybe A), mientras que los tipos que aceptan valores NULL no lo hacen ( String??= String?).
En teoría de tipos , puede escribirse como: . Esto expresa el hecho de que para un conjunto dado de valores en , un tipo de opción agrega exactamente un valor adicional (el valor vacío) al conjunto de valores válidos para . Esto se refleja en la programación por el hecho de que en los lenguajes que tienen uniones etiquetadas , los tipos de opción pueden expresarse como la unión etiquetada del tipo encapsulado más un tipo de unidad . [1]
En la correspondencia de Curry-Howard , los tipos de opciones están relacionados con la ley de aniquilación para ∨: x∨1=1. [ ¿cómo? ]
Un tipo de opción también se puede ver como una colección que contiene uno o cero elementos. [ investigación original? ]
Ada no implementa tipos de opciones directamente, sin embargo, proporciona tipos discriminados que se pueden usar para parametrizar un registro. Para implementar un tipo de opción, se utiliza un tipo booleano como discriminante; el siguiente ejemplo proporciona un genérico para crear un tipo de opción a partir de cualquier tipo restringido no limitado: