programming-languages - probabilidades - union de conjuntos

Tipos de unión y tipos de intersección

Question

¿Cuáles son los diversos casos de uso para tipos de unión e intersección? Últimamente ha habido mucho alboroto sobre estas características del sistema de tipo, ¡pero de alguna manera nunca sentí necesidad de ninguna de estas!

Answer 1

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

type JObject = Map[String, JValue]
type JArray = List[JValue]
type JValue = String | Number | Bool | Null | JObject | JArray
type Json = JObject | JArray

def stringify(json: JValue): String = json match {
    case String | Number | Bool | Null => json.toString()
    case JObject => "{" + json.map(x y => x + ": " + stringify(y)).mkStr(", ") + "}"
    case JArray => "[" + json.map(stringify).mkStr(", ") + "]"
}

Answer 2

Si quieres una respuesta más práctica:

Con los tipos de unión y recursivos puede codificar tipos de árbol regulares y, por lo tanto, tipos de XML.

Con los tipos de intersección puede escribir AMBAS funciones sobrecargadas y tipos de refinamiento (lo que en una publicación anterior se llama sobrecarga coherente)

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

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) -> String

Pero también puede refinar el tipo de arriba y escribir la función de arriba como

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

donde Pos y Neg son tipos enteros positivos y negativos.

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

Si quiere probarlo y está en Linux, entonces probablemente esté incluido en su distribución (apt-get install cduce o yum install cduce debería funcionar) y puede usar su nivel superior (a la OCaml) para jugar con union y tipos de intersección. En el sitio de CDuce encontrará muchos ejemplos prácticos de uso de los tipos de unión e intersección. Y como 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 los tipos de suma ML (consulte here ).

Aquí tiene un ejemplo complejo que combina los tipos de unión e intersección (explicado en la página "http://www.cduce.org/tutorial_overloading.html#val"), pero para comprenderlo, debe comprender la comparación de patrones de expresiones regulares, 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, transforma los valores de tipo Person en valores de tipo (Man | Women) (donde la barra vertical denota un tipo de unión) pero manteniendo la correspondencia entre los géneros: split es una función con tipo de intersección

MPerson -> Man & FPerson -> Woman

Answer 3

Los tipos de unión son útiles para escribir lenguajes dinámicos o, de lo contrario, permiten una mayor flexibilidad en los tipos pasados ​​que la mayoría de los lenguajes estáticos. Por ejemplo, considera esto:

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

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

Un uso para los tipos de intersección es describir un objeto que implementa múltiples interfaces. Por ejemplo, C # permite múltiples restricciones de interfaz 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 de arg es la intersección de IFoo e IBar . Usando eso, el comprobador de tipos sabe que tanto Foo() como Bar() son métodos válidos en él.

Answer 4

Tipos de union

Para citar a Robert Harper, "Fundamentos prácticos para lenguajes de programación", capítulo 15:

La mayoría de las estructuras de datos implican alternativas como la distinción entre una hoja y un nodo interior en un árbol, o una elecció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 las hojas no, y así sucesivamente. Estos conceptos se expresan por tipos de suma , específicamente la suma binaria, que ofrece una opción de dos cosas, y la suma nula, que ofrece una opción de no cosas.

Booleanos

El tipo de suma más simple es el booleano,

data Bool = True
          | False

Los booleanos solo tienen dos valores válidos, T o F. Por lo tanto, en lugar de representarlos como números, podemos usar un tipo de suma para codificar con mayor precisión el hecho de que solo hay dos valores posibles.

Enumeraciones

Las enumeraciones son ejemplos de tipos de suma más generales: unos con muchos, pero valores finitos, alternativos.

Suma de tipos y punteros nulos.

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

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

data Maybe a = Nothing
             | Just a

donde podemos distinguir entre valores válidos e inválidos utilizando la etiqueta Nothing o Just para anotar cada valor con su estado.

Al usar los tipos de suma de esta manera, podemos descartar por completo los errores de puntero nulo, lo que es un ejemplo motivador bastante decente. Los punteros nulos se deben en su totalidad a la incapacidad de los idiomas antiguos para expresar tipos de suma fácilmente.

Tipos de interseccion

Los tipos de intersección son mucho más nuevos y sus aplicaciones no se comprenden tan ampliamente. Sin embargo, la tesis de Benjamin Pierce ("Programación con tipos de intersección y polimorfismo delimitado") ofrece una buena descripción general:

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

Por ejemplo, a la función de suma (+) se le puede dar el tipo Int -> Int -> Int ^ Real -> Real -> Real , capturando el hecho general de que la suma de dos números reales es siempre real y la más especializada. hecho de que la suma de dos enteros es siempre un entero. Un compilador para un idioma con tipos de intersección podría incluso proporcionar dos secuencias diferentes de código de objeto para las dos versiones de (+) , una con una instrucción de suma de punto flotante y otra con suma de enteros. Para cada instancia de + en un programa, el compilador puede decidir si ambos argumentos son enteros y generar la secuencia de código de objeto más eficiente en este caso.

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

Nos permiten 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,