¿Qué es un tipo existencial?

Leí el artículo de Wikipedia Tipos existenciales . Supuse que se llaman tipos existenciales debido al operador existencial (∃). Sin embargo, no estoy seguro de cuál es el punto. Cuál es la diferencia entre

T = ∃X { X a; int f(X); }

y

T = ∀x { X a; int f(X); }

?

Cuando alguien define un tipo universal ∀X, está diciendo: puede conectar el tipo que desee, no necesito saber nada sobre el tipo para hacer mi trabajo, solo me referiré a él de forma opacaX .

Cuando alguien define un tipo existencial ∃X, está diciendo: usaré el tipo que quiera aquí; no sabrá nada sobre el tipo, por lo que solo puede referirse a él opacamente comoX .

Los tipos universales le permiten escribir cosas como:

void copy<T>(List<T> source, List<T> dest) {
   ...
}

La copyfunción no tiene idea de lo Tque realmente será, pero no es necesario.

Los tipos existenciales te permitirían escribir cosas como:

interface VirtualMachine<B> {
   B compile(String source);
   void run(B bytecode);
}

// Now, if you had a list of VMs you wanted to run on the same input:
void runAllCompilers(List<∃B:VirtualMachine<B>> vms, String source) {
   for (∃B:VirtualMachine<B> vm : vms) {
      B bytecode = vm.compile(source);
      vm.run(bytecode);
   }
}

Cada implementación de máquina virtual en la lista puede tener un tipo de código de bytes diferente. La runAllCompilersfunción no tiene idea de cuál es el tipo de código de bytes, pero no es necesario; todo lo que hace es transmitir el bytecode de VirtualMachine.compilea VirtualMachine.run.

Los comodines de tipo Java (ej . List<?>:) son una forma muy limitada de tipos existenciales.

Actualización: Olvidé mencionar que puede simular tipos existenciales con tipos universales. Primero, ajuste su tipo universal para ocultar el parámetro de tipo. Segundo, invierta el control (esto efectivamente intercambia la parte "usted" y "yo" en las definiciones anteriores, que es la diferencia principal entre existenciales y universales).

// A wrapper that hides the type parameter 'B'
interface VMWrapper {
   void unwrap(VMHandler handler);
}

// A callback (control inversion)
interface VMHandler {
   <B> void handle(VirtualMachine<B> vm);
}

Ahora podemos tener la VMWrapperllamada propia VMHandlerque tiene una handlefunción de tipo universal . El efecto neto es el mismo, nuestro código debe tratarse Bcomo opaco.

void runWithAll(List<VMWrapper> vms, final String input)
{
   for (VMWrapper vm : vms) {
      vm.unwrap(new VMHandler() {
         public <B> void handle(VirtualMachine<B> vm) {
            B bytecode = vm.compile(input);
            vm.run(bytecode);
         }
      });
   }
}

Un ejemplo de implementación de VM:

class MyVM implements VirtualMachine<byte[]>, VMWrapper {
   public byte[] compile(String input) {
      return null; // TODO: somehow compile the input
   }
   public void run(byte[] bytecode) {
      // TODO: Somehow evaluate 'bytecode'
   }
   public void unwrap(VMHandler handler) {
      handler.handle(this);
   }
}

Un valor de un tipo existencial como ∃x. F(x) es un par que contiene algún tipo x y un valor del tipo F(x). Mientras que un valor de tipo polimórfico como ∀x. F(x)es una función que toma algún tipo xy produce un valor de tipo F(x). En ambos casos, el tipo se cierra sobre algún tipo de constructor F.

Tenga en cuenta que esta vista combina tipos y valores. La prueba existencial es de un tipo y un valor. La prueba universal es una familia completa de valores indexados por tipo (o una asignación de tipos a valores).

Entonces, la diferencia entre los dos tipos que especificó es la siguiente:

T = ∃X { X a; int f(X); }

Esto significa: Un valor de tipo Tcontiene un tipo llamado X, un valor a:Xy una función f:X->int. Un productor de valores de tipo Tpuede elegir cualquier tipo Xy un consumidor no puede saber nada al respecto X. Excepto que hay un ejemplo de que se llama ay que este valor se puede convertir en un intdándolo a f. En otras palabras, un valor de tipo Tsabe producir de intalguna manera. Bueno, podríamos eliminar el tipo intermedio Xy solo decir:

T = int

El universalmente cuantificado es un poco diferente.

T = ∀X { X a; int f(X); }

Esto significa: un valor de tipo Tpuede recibir cualquier tipo X, y producirá un valor a:Xy una función f:X->int sin importar cuál Xsea . En otras palabras: un consumidor de valores de tipo Tpuede elegir cualquier tipo de X. Y un productor de valores de tipo Tno puede saber nada en absoluto X, pero tiene que ser capaz de producir un valor apara cualquier elección Xy poder convertir dicho valor en un int.

Obviamente, implementar este tipo es imposible, porque no hay un programa que pueda producir un valor de cada tipo imaginable. A menos que permita absurdos como nullo fondos.

Como un existencial es un par, un argumento existencial puede convertirse en uno universal mediante currículum .

(∃b. F(b)) -> Int

es lo mismo que:

∀b. (F(b) -> Int)

El primero es un existencial de rango 2 . Esto lleva a la siguiente propiedad útil:

Todo tipo de rango existencialmente cuantificado n+1es un tipo de rango universalmente cuantificado n.

Existe un algoritmo estándar para convertir los existenciales en universales, llamado Skolemization .

Creo que tiene sentido explicar los tipos existenciales junto con los tipos universales, ya que los dos conceptos son complementarios, es decir, uno es el "opuesto" del otro.

No puedo responder a cada detalle sobre los tipos existenciales (como dar una definición exacta, enumerar todos los usos posibles, su relación con los tipos de datos abstractos, etc.) porque simplemente no tengo el conocimiento suficiente para eso. Solo demostraré (usando Java) lo que este artículo de HaskellWiki dice que es el efecto principal de los tipos existenciales:

Los tipos existenciales se pueden usar para varios propósitos diferentes. Pero lo que hacen es 'ocultar' una variable de tipo en el lado derecho. Normalmente, cualquier variable de tipo que aparezca a la derecha también debe aparecer a la izquierda […]

Ejemplo de configuración:

El siguiente pseudocódigo no es Java válido, a pesar de que sería lo suficientemente fácil de solucionar. De hecho, ¡eso es exactamente lo que voy a hacer en esta respuesta!

class Tree<α>
{
    α       value;
    Tree<α> left;
    Tree<α> right;
}

int height(Tree<α> t)
{
    return (t != null)  ?  1 + max( height(t.left), height(t.right) )
                        :  0;
}

Déjame explicarte esto brevemente. Estamos definiendo ...

• Un tipo recursivo Tree<α>que representa un nodo en un árbol binario. Cada nodo almacena un valuetipo de α y tiene referencias a subtítulos opcionales lefty rightdel mismo tipo.

• una función heightque devuelve la distancia más lejana desde cualquier nodo hoja al nodo raíz t.

¡Ahora, cambiemos el pseudocódigo anterior heighta la sintaxis Java correcta! (Seguiré omitiendo algunas repeticiones por razones de brevedad, como la orientación a objetos y los modificadores de accesibilidad). Voy a mostrar dos posibles soluciones.

1. Solución de tipo universal:

La solución más obvia es simplemente hacer heightgenérico introduciendo el parámetro de tipo α en su firma:

<α> int height(Tree<α> t)
{
    return (t != null)  ?  1 + max( height(t.left), height(t.right) )
                        :  0;
}

Esto le permitiría declarar variables y crear expresiones de tipo α dentro de esa función, si así lo desea. Pero...

2. Solución de tipo existencial:

Si observa el cuerpo de nuestro método, notará que en realidad no estamos accediendo o trabajando con nada del tipo α . No hay expresiones que tengan ese tipo, ni ninguna variable declarada con ese tipo ... entonces, ¿por qué tenemos que hacer algo heightgenérico? ¿Por qué no podemos simplemente olvidarnos de α ? Como resultado, podemos:

int height(Tree<?> t)
{
    return (t != null)  ?  1 + max( height(t.left), height(t.right) )
                        :  0;
}

Como escribí al comienzo de esta respuesta, los tipos existenciales y universales son de naturaleza complementaria / dual. Por lo tanto, si la solución de tipo universal fuera hacer height más genérico, entonces deberíamos esperar que los tipos existenciales tengan el efecto contrario: hacerlo menos genérico, es decir, al ocultar / eliminar el parámetro de tipo α .

Como consecuencia, ya no puede hacer referencia al tipo de t.valueen este método ni manipular ninguna expresión de ese tipo, porque no se ha vinculado ningún identificador. (El ?comodín es un token especial, no un identificador que "captura" un tipo). De hecho, se t.valueha vuelto opaco; tal vez lo único que aún puede hacer con él es moldearlo Object.

Resumen:

===========================================================
                     |    universally       existentially
                     |  quantified type    quantified type
---------------------+-------------------------------------
 calling method      |                  
 needs to know       |        yes                no
 the type argument   |                 
---------------------+-------------------------------------
 called method       |                  
 can use / refer to  |        yes                no  
 the type argument   |                  
=====================+=====================================

Todos estos son buenos ejemplos, pero elijo responderlo un poco diferente. Recordemos de las matemáticas, que ∀x. P (x) significa "para todas las x, puedo probar que P (x)". En otras palabras, es un tipo de función, me das una x y tengo un método para demostrártelo.

En teoría de tipos, no estamos hablando de pruebas, sino de tipos. Entonces en este espacio queremos decir "para cualquier tipo X que me des, te daré un tipo P específico". Ahora, dado que no le damos a P mucha información sobre X además del hecho de que es un tipo, P no puede hacer mucho con él, pero hay algunos ejemplos. P puede crear el tipo de "todos los pares del mismo tipo": P<X> = Pair<X, X> = (X, X). O podemos crear el tipo de opción:, P<X> = Option<X> = X | Nildonde Nil es el tipo de punteros nulos. Podemos hacer una lista fuera de él: List<X> = (X, List<X>) | Nil. Observe que el último es recursivo, los valores de List<X>son pares donde el primer elemento es una X y el segundo elemento es un List<X>o es un puntero nulo.

Ahora, en matemáticas ∃x. P (x) significa "Puedo probar que hay una x particular de tal manera que P (x) es verdadera". Puede haber muchas de esas x, pero para demostrarlo, una es suficiente. Otra forma de pensarlo es que debe existir un conjunto no vacío de pares de evidencia y prueba {(x, P (x))}.

Traducido a la teoría de tipos: Un tipo en la familia ∃X.P<X>es un tipo X y un tipo correspondiente P<X>. Tenga en cuenta que mientras antes le dimos X a P, (para que supiéramos todo sobre X pero P muy poco), lo contrario es cierto ahora. P<X>no promete dar ninguna información sobre X, solo que hay una, y que de hecho es un tipo.

¿Cómo es esto útil? Bueno, P podría ser un tipo que tiene una forma de exponer su tipo interno X. Un ejemplo sería un objeto que oculta la representación interna de su estado X. Aunque no tenemos forma de manipularlo directamente, podemos observar su efecto mediante hurgando en P. Podría haber muchas implementaciones de este tipo, pero podría usar todos estos tipos sin importar cuál se eligió en particular.

Para responder directamente a su pregunta:

Con el tipo universal, los usos de Tdeben incluir el parámetro de tipo X. Por ejemplo T<String>o T<Integer>. Para los usos de tipo existenciales de Tno incluya ese parámetro de tipo porque es desconocido o irrelevante, solo use T(o en Java T<?>).

Más información:

Los tipos universales / abstractos y los tipos existenciales son una dualidad de perspectiva entre el consumidor / cliente de un objeto / función y el productor / implementación del mismo. Cuando un lado ve un tipo universal, el otro ve un tipo existencial.

En Java puedes definir una clase genérica:

public class MyClass<T> {
   // T is existential in here
   T whatever; 
   public MyClass(T w) { this.whatever = w; }

   public static MyClass<?> secretMessage() { return new MyClass("bazzlebleeb"); }
}

// T is universal from out here
MyClass<String> mc1 = new MyClass("foo");
MyClass<Integer> mc2 = new MyClass(123);
MyClass<?> mc3 = MyClass.secretMessage();

• Desde la perspectiva de un cliente de MyClass, Tes universal porque se puede sustituir cualquier tipo para Tcuando se utiliza esa clase y se debe conocer el tipo real de T cada vez que utilice una instancia deMyClass
• Desde la perspectiva de los métodos de instancia en MyClasssí mismo, Tes existencial porque no conoce el tipo real deT
• En Java, ?representa el tipo existencial, por lo tanto, cuando estás dentro de la clase, Tes básicamente ?. Si desea manejar una instancia de MyClasscon Texistencial, puede declarar MyClass<?>como en el secretMessage()ejemplo anterior.

Los tipos existenciales a veces se usan para ocultar los detalles de implementación de algo, como se discutió en otra parte. Una versión Java de esto podría verse así:

public class ToDraw<T> {
    T obj;
    Function<Pair<T,Graphics>, Void> draw;
    ToDraw(T obj, Function<Pair<T,Graphics>, Void>
    static void draw(ToDraw<?> d, Graphics g) { d.draw.apply(new Pair(d.obj, g)); }
}

// Now you can put these in a list and draw them like so:
List<ToDraw<?>> drawList = ... ;
for(td in drawList) ToDraw.draw(td);

Es un poco complicado capturar esto correctamente porque pretendo estar en algún tipo de lenguaje de programación funcional, que Java no es. Pero el punto aquí es que está capturando algún tipo de estado más una lista de funciones que operan en ese estado y no conoce el tipo real de la parte del estado, pero las funciones sí lo saben ya que ya estaban emparejadas con ese tipo .

Ahora, en Java, todos los tipos no finales no primitivos son parcialmente existenciales. Esto puede sonar extraño, pero debido a que una variable declarada como Objectpotencialmente podría ser una subclase Object, no puede declarar el tipo específico, solo "este tipo o una subclase". Por lo tanto, los objetos se representan como un bit de estado más una lista de funciones que operan en ese estado: exactamente qué función llamar se determina en tiempo de ejecución por búsqueda. Esto es muy parecido al uso de los tipos existenciales anteriores donde tiene una parte de estado existencial y una función que opera en ese estado.

En lenguajes de programación con tipos estáticos sin subtipos y conversiones, los tipos existenciales le permiten a uno administrar listas de objetos con tipos diferentes. Una lista de T<Int>no puede contener a T<Long>. Sin embargo, una lista de T<?>puede contener cualquier variación de T, lo que permite colocar muchos tipos diferentes de datos en la lista y convertirlos a un int (o hacer cualquier operación que se proporcione dentro de la estructura de datos) a pedido.

Casi siempre se puede convertir un registro con un tipo existencial en un registro sin usar cierres. Un cierre también se escribe existencialmente, ya que las variables libres sobre las que se cierra están ocultas para la persona que llama. Por lo tanto, un lenguaje que admite cierres pero no tipos existenciales puede permitirle hacer cierres que compartan el mismo estado oculto que habría puesto en la parte existencial de un objeto.

Un tipo existencial es un tipo opaco.

Piense en un identificador de archivo en Unix. Sabes que su tipo es int, por lo que puedes falsificarlo fácilmente. Puede, por ejemplo, intentar leer desde el identificador 43. Si sucede que el programa tiene un archivo abierto con este identificador en particular, lo leerá. Su código no tiene que ser malicioso, solo descuidado (por ejemplo, el identificador podría ser una variable no inicializada).

Un tipo existencial está oculto de su programa. Si se fopendevuelve un tipo existencial, todo lo que podría hacer con él es usarlo con algunas funciones de biblioteca que acepten este tipo existencial. Por ejemplo, se compilaría el siguiente pseudocódigo:

let exfile = fopen("foo.txt"); // No type for exfile!
read(exfile, buf, size);

La interfaz "leer" se declara como:

Existe un tipo T tal que:

size_t read(T exfile, char* buf, size_t size);

La variable exfile no es un char*archivo int, ni un archivo struct, nada que pueda expresar en el sistema de tipos. No puede declarar una variable cuyo tipo es desconocido y no puede lanzar, por ejemplo, un puntero a ese tipo desconocido. El idioma no te deja.

Parece que llego un poco tarde, pero de todos modos, este documento agrega otra visión de lo que son los tipos existenciales, aunque no es específicamente agnóstico al lenguaje, debería ser bastante más fácil de entender los tipos existenciales: http: //www.cs.uu .nl / groups / ST / Projects / ehc / ehc-book.pdf (capítulo 8)

La diferencia entre un tipo cuantificado universalmente y existencialmente puede caracterizarse por la siguiente observación:

• El uso de un valor con un tipo cuantificado determines determina el tipo a elegir para la instanciación de la variable de tipo cuantificado. Por ejemplo, el llamador de la función de identidad "id :: ∀aa → a" determina el tipo a elegir para la variable de tipo a para esta aplicación particular de id. Para la aplicación de función "id 3", este tipo es igual a Int.

• La creación de un valor con un tipo cuantificado determines determina y oculta el tipo de la variable de tipo cuantificado. Por ejemplo, un creador de un "∃a. (A, a → Int)" puede haber construido un valor de ese tipo a partir de "(3, λx → x)"; otro creador ha construido un valor con el mismo tipo a partir de "('x', λx → ord x)". Desde el punto de vista de los usuarios, ambos valores tienen el mismo tipo y, por lo tanto, son intercambiables. El valor tiene un tipo específico elegido para la variable de tipo a, pero no sabemos qué tipo, por lo que esta información ya no se puede explotar. Esta información de tipo específica de valor ha sido 'olvidada'; solo sabemos que existe.

Existe un tipo universal para todos los valores de los parámetros de tipo. Un tipo existencial existe solo para valores de los parámetros de tipo que satisfacen las restricciones del tipo existencial.

Por ejemplo, en Scala, una forma de expresar un tipo existencial es un tipo abstracto que está limitado a algunos límites superiores o inferiores.

trait Existential {
  type Parameter <: Interface
}

De manera equivalente, un tipo universal restringido es un tipo existencial como en el siguiente ejemplo.

trait Existential[Parameter <: Interface]

Cualquier sitio de uso puede emplear el Interfaceporque cualquier subtipo de instancia de Existentialdebe definir el type Parameterque debe implementar el Interface.

Un caso degenerado de un tipo existencial en Scala es un tipo abstracto al que nunca se hace referencia y, por lo tanto, no necesita ser definido por ningún subtipo. Esto efectivamente tiene una notación abreviada de List[_] en Scala y List<?>en Java.

Mi respuesta se inspiró en la propuesta de Martin Odersky de unificar tipos abstractos y existenciales. La diapositiva adjunta ayuda a la comprensión.

La investigación de tipos de datos abstractos y el ocultamiento de información trajeron tipos existenciales a lenguajes de programación. Hacer un resumen de tipo de datos oculta información sobre ese tipo, por lo que un cliente de ese tipo no puede abusar de él. Digamos que tiene una referencia a un objeto ... algunos lenguajes le permiten convertir esa referencia a una referencia a bytes y hacer lo que quiera con ese trozo de memoria. Con el fin de garantizar el comportamiento de un programa, es útil que un lenguaje imponga que solo actúes sobre la referencia al objeto a través de los métodos que proporciona el diseñador del objeto. Sabes que el tipo existe, pero nada más.

Ver:

Los tipos abstractos tienen tipo existencial, MITCHEL y PLOTKIN

http://theory.stanford.edu/~jcm/papers/mitch-plotkin-88.pdf

Creé este diagrama. No sé si es riguroso. Pero si ayuda, me alegro.

Según tengo entendido, es una forma matemática de describir interfaces / clase abstracta.

En cuanto a T = ∃X {X a; int f (X); }

Para C # se traduciría a un tipo abstracto genérico:

abstract class MyType<T>{
    private T a;

    public abstract int f(T x);
}

"Existencial" solo significa que hay algún tipo que obedece a las reglas definidas aquí.