Tipos de unión y tipos de intersección

Question

¿Cuáles son los diversos casos de uso para tipos de unión y tipos de intersección? Ultimamente se ha hablado mucho sobre estas características del sistema de tipo, ¡pero de alguna manera nunca sentí la necesidad de ninguno de estos!

Tipos

Answer 1

Si desea una respuesta orientada a la práctica más:

Con la unión y tipos recursivos que puede codificar tipos de árboles regulares y por lo tanto tipos XML.

Con tipos de intersección se puede escribir ambas funciones sobrecargadas y tipos de refinamiento (lo que en un post anterior se llama sobrecarga coherente)

Así, por ejemplo, se puede escribir la función de complemento (que sobrecarga suma de enteros y la concatenación de cadenas) como siguiente

let add ((Int,Int)->Int ; (String,String)->String) 
     | (x & Int, y & Int) -> x+y 
     | (x & String, y & String) -> x@y ;; 

que tiene el tipo de intersección

(Int, Int) -> Int & (String, String) -> cadena

Pero también se puede refinar el tipo anterior y escriba la función anterior como

(Pos,Pos) -> Pos & 
(Neg,Neg) -> Neg & 
(Int,Int)->Int & 
(String,String)->String. 

donde Pos Neg y son los tipos enteros positivos y negativos.

El código anterior es ejecutable en el lenguaje CDuce (http://www.cduce.org) cuyo tipo de sistema incluye unión, intersecciones y tipos de negación (está principalmente dirigido a transformaciones XML).

Si quieres probarlo y estás en Linux, entonces probablemente esté incluido en tu distribución (apt-get install cduce o yum install cduce debería hacer el trabajo) y puedes usar su toplevel (a la OCaml) para jugar con los tipos de unión e intersección. En el sitio de CDuce encontrará una gran cantidad de ejemplos prácticos de uso de tipos de unión e intersección. Y dado que hay una integración completa con las bibliotecas OCaml (puede importar bibliotecas OCaml en CDuce y exportar módulos CDuce a OCaml) también puede verificar la correspondencia con tipos de suma ML (consulte here).

Aquí tienes un ejemplo complejo que mezcla los tipos de unión e intersección (explicado en la página "http://www.cduce.org/tutorial_overloading.html#val"), pero para entenderlo debes entender la expresión regular coincidencia de patrones, que requiere un poco de esfuerzo.

type Person = FPerson | MPerson 
type FPerson = <person gender = "F">[ Name Children ] 
type MPerson = <person gender = "M">[ Name Children ] 
type Children = <children>[ Person* ] 
type Name  = <name>[ PCDATA ] 

type Man = <man name=String>[ Sons Daughters ] 
type Woman = <woman name=String>[ Sons Daughters ] 
type Sons = <sons>[ Man* ] 
type Daughters = <daughters>[ Woman* ] 

let fun split (MPerson -> Man ; FPerson -> Woman) 
    <person gender=g>[ <name>n <children>[(mc::MPerson | fc::FPerson)*] ] -> 
    (* the above pattern collects all the MPerson in mc, and all the FPerson in fc *) 
    let tag = match g with "F" -> `woman | "M" -> `man in 
    let s = map mc with x -> split x in 
    let d = map fc with x -> split x in  
    <(tag) name=n>[ <sons>s <daughters>d ] ;; 

En pocas palabras se transforma valores de tipo Persona en valores de tipo (Hombre | Mujeres) (donde la barra vertical indica un tipo de unión), pero manteniendo la correspondencia entre los géneros: división es una función con intersección tipo

MPerson -> Man & FPerson -> Woman 

Answer 2

Unión

para citar a Robert Harper, "Fundamentos prácticos de programación idiomas", ch 15:

La mayoría de las estructuras de datos implican alternativas tales como la distinción entre una hoja y un nodo interior en un árbol, o una opción en la forma más externa de una pieza de sintaxis abstracta. Es importante destacar que la elección determina la estructura del valor. Por ejemplo, los nodos tienen hijos, pero no los deja no, y así sucesivamente. Estos conceptos son expresados ​​por suma tipos, específicamente la suma binaria, que ofrece una opción de dos cosas, y la suma nulary, que ofrece una opción de nada.

Booleanos

El tipo más simple suma es la de Boole,

data Bool = True 
      | False 

Booleanos tener sólo dos valores válidos, T o F. Así que en lugar de representarlos como números, que puede en vez use un tipo de suma para codificar con mayor precisión el hecho de que solo hay dos valores posibles.

Enumeraciones

enumeraciones son ejemplos de tipos de suma más generales: los que tienen muchos, pero finitas, valores alternativos.

tipos de suma y punteros nulos

El mejor ejemplo de motivación para prácticamente tipos suma es discriminar entre los resultados válidos y los valores de error devueltos por funciones, distinguiendo el caso fracaso.

Por ejemplo, punteros nulos y los caracteres de fin de archivo son codificaciones hacker del tipo suma:

data Maybe a = Nothing 
      | Just a 

donde podemos distinguir entre los valores válidos y no válidos mediante el uso de la etiqueta Nothing o Just para anotar cada uno valor con su estado.

Al usar los tipos de suma de esta forma, podemos descartar por completo los errores de puntero nulos, lo cual es un ejemplo bastante motivador. Los punteros nulos se deben completamente a la incapacidad de los idiomas antiguos para expresar tipos de suma fácilmente.

Tipos de intersección

tipos de intersecciones son mucho más recientes, y sus aplicaciones no se entienden tan ampliamente.Sin embargo, la tesis de Benjamin Pierce ("Programación con tipos de intersección y limitada Polimorfismo") ofrece una buena panorámica:

El más intrigante y potencialmente propiedad útil de los tipos de intersección es su capacidad para expresar una esencialmente ilimitada (aunque de curso finito) cantidad de información sobre los componentes de un programa.

Para ejemplo, la función de suma (+) puede ser dado el tipo Int -> Int -> Int^Real -> Real -> Real, capturando tanto el hecho general que la suma de dos números reales es siempre una real y lo más hecho especializada que la suma de dos enteros es siempre un entero. A compilador para un lenguaje con tipos de intersección podría incluso proporcionar dos diferentes secuencias de código de objeto para las dos versiones de (+), uno utilizando una instrucción de adición punto flotante fl y uno usando Además entero. Para cada instancia de + en un programa, el compilador puede decidir si ambos argumentos son enteros y generan la secuencia de código de objeto más eficiente en este caso.

Este tipo de fi nitary polimorfismo o coherente sobrecarga es tan expresiva, que ... el conjunto de todas las tipificaciones válidas para un programa equivale a una caracterización completa del comportamiento del programa

Ellos vamos a codificar una gran cantidad de información en el tipo, explicando a través de la teoría de tipos lo que significa herencia múltiple, dando tipos a las clases de tipo,

Answer 3

tipos de unión son útil para escribir en lenguajes dinámicos o de otra manera permitir más flexibilidad en los tipos pasados ​​que la mayoría de los lenguajes estáticos permiten. Por ejemplo, considere esto:

var a; 
if (condition) { 
    a = "string"; 
} else { 
    a = 123; 
} 

Si tiene tipos de unión, es fácil de escribir a como int | string.

Un uso para tipos de intersección es describir un objeto que implementa múltiples interfaces. Por ejemplo, C# permite que múltiples interface constraints en genéricos:

interface IFoo { 
    void Foo(); 
} 

interface IBar { 
    void Bar(); 
} 

void Method<T>(T arg) where T : IFoo, IBar { 
    arg.Foo(); 
    arg.Bar(); 
} 

Aquí, el tipo arg 's es la intersección de IFoo y IBar. Usando eso, el verificador de tipos sabe ambosFoo() y Bar() son métodos válidos en él.

Answer 4

Por ejemplo, con los tipos de unión se podría describir el modelo de dominio json sin introducir nuevas clases reales, pero utilizando únicamente alias de tipo.