language agnostic - ¿Qué es un tipo existencial?
language-agnostic types (10)
Leí el artículo de Wikipedia Tipos existenciales . Descubrí que se llaman tipos existenciales debido al operador existencial (∃). Aunque 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); }
?
Como entiendo, es una manera 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í.
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 todos los detalles sobre los tipos existenciales (como dar una definición exacta, enumerar todos los usos posibles, su relación con tipos de datos abstractos, etc.) porque simplemente no estoy lo suficientemente informado para eso. Demostraré solo (usando Java) lo que este artículo de HaskellWiki declara 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 completamente válido para Java, aunque sería bastante fácil corregirlo. 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;
}
Permíteme deletrearlo brevemente por ti. Estamos definiendo ...
un
Tree<α>tipo recursivoTree<α>que representa un nodo en un árbol binario. Cada nodo almacena unvaluede algún tipo α y tiene referencias a subárboles opcionalesleftyrightdel mismo tipo.una
heightfunción que devuelve la distancia más alejada de cualquier nodo hoja al nodo raízt.
Ahora, convirtamos el pseudocódigo anterior de height en la sintaxis de Java adecuada. (Continuaré omitiendo un texto repetitivo por motivos de brevedad, como la orientación a objetos y modificadores de accesibilidad). Mostraré dos posibles soluciones.
1. Solución de tipo universal:
La solución más obvia es simplemente hacer que la height genérica 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 nos fijamos en el cuerpo de nuestro método, observará 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 que la height genérica? ¿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 que la height más genérica, entonces deberíamos esperar que los tipos existenciales tengan el efecto opuesto: haciéndolo menos genérico, es decir, ocultando / eliminando el parámetro de tipo α .
Como consecuencia, ya no puede referirse al tipo de t.value en este método ni manipular ninguna expresión de ese tipo, porque ningún identificador ha estado vinculado a él. (El comodín ? Es un token especial, no un identificador que "captura" un tipo). t.value ha vuelto efectivamente opaco; quizás lo único que todavía puede hacer con él es escribirlo en 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 |
=====================+=====================================
Cuando alguien define un tipo universal ∀X , dicen: puedes conectar el tipo que quieras, no necesito saber nada sobre el tipo para hacer mi trabajo, solo me referiré a él de forma opaca como X
Cuando alguien define un tipo existencial ∃X , dicen: ∃X tipo que quiera aquí; no sabrá nada sobre el tipo, por lo que solo puede referirse a él de forma opaca como X
Los tipos universales le permiten escribir cosas como:
void copy<T>(List<T> source, List<T> dest) {
...
}
La función de copy no tiene idea de qué será T realidad, pero no es necesario.
Los tipos existenciales te permiten 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 byte diferente. La función runAllCompilers no tiene idea de qué es el tipo de bytecode, pero no es necesario; todo lo que hace es transmitir el bytecode de VirtualMachine.compile a VirtualMachine.run .
Los comodines de tipo Java (por ejemplo, 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. En segundo lugar, invierta el control (esto efectivamente intercambia la parte "usted" y "yo" en las definiciones anteriores, que es la principal diferencia entre los 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 hacer que VMWrapper llame a nuestro propio VMHandler que tiene una función de handle tipo universal. El efecto neto es el mismo, nuestro código tiene que tratar a B como 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);
}
}
Existe un tipo universal para todos los valores del parámetro (s) de tipo. Existe un tipo existencial solo para los 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á restringido a algunos límites superiores o inferiores.
trait Existential {
type Parameter <: Interface
}
De forma equivalente, un tipo universal restringido es un tipo existencial como en el siguiente ejemplo.
trait Existential[Parameter <: Interface]
Cualquier sitio de uso puede emplear la Interface porque cualquier subtipo de Existential que pueda ser instanciado debe definir el type Parameter que debe implementar la Interface .
Un caso degenerado de 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 fue inspirada por la propuesta de Martin Odersky de unificar tipos abstractos y existenciales. La diapositiva que lo acompaña ayuda a comprender.
La investigación de los tipos de datos abstractos y el ocultamiento de la información trajo tipos existenciales a los 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 idiomas le permiten convertir esa referencia a una referencia a bytes y hacer lo que quiera con esa pieza de memoria. A los efectos de garantizar el comportamiento de un programa, es útil para un lenguaje exigir que solo actúe sobre la referencia al objeto a través de los métodos proporcionados por el diseñador del objeto. Usted sabe que existe el tipo, pero nada más.
Ver:
Los tipos abstractos tienen tipo existencial, MITCHEL y PLOTKIN
Para responder directamente a tu pregunta:
Con el tipo universal, los usos de T deben incluir el parámetro de tipo X Por ejemplo, T<String> o T<Integer> . Para los usos de tipo existencial de T , no incluya ese parámetro de tipo porque es desconocido o irrelevante; simplemente 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 puede sustituir cualquier tipo porTcuando usa esa clase y debe saber el tipo real de T cada vez que utiliza una instancia deMyClass - Desde la perspectiva de los métodos de instancia en
MyClass,Tes existencial porque no conoce el tipo real deT - En Java
?representa el tipo existencial - ¿así que cuando estás dentro de la clase,Tes básicamente?. Si desea manejar una instancia deMyClassconTexistencial, puede declararMyClass<?>Como en el ejemplo desecretMessage()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 de 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 usted no sabe el tipo real de la parte de estado, pero las funciones sí lo hacen, ya que ya estaban emparejadas con ese tipo. .
Ahora, en Java, todos los tipos no primitivos no primitivos son en parte existenciales. Esto puede sonar extraño, pero como una variable declarada como Object podría ser una subclase de Object lugar, no puede declarar el tipo específico, solo "este tipo o una subclase". Y así, los objetos se representan como un poco 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 mediante búsqueda. Esto es muy parecido al uso de tipos existenciales arriba donde tiene una parte de estado existencial y una función que opera en ese estado.
En los lenguajes de programación tipados estáticamente sin subtipificación y moldes, los tipos existenciales permiten administrar listas de objetos de tipos diferentes. Una lista de T<Int> no puede contener un T<Long> . Sin embargo, una lista de T<?> Puede contener cualquier variación de T , permitiéndole poner 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) bajo demanda.
Uno puede casi siempre convertir un registro con un tipo existencial en un registro sin usar cierres. Un cierre también se escribe de forma existencial, ya que las variables libres sobre las que se cierra están ocultas para quien llama. Por lo tanto, un lenguaje que admite cierres pero no tipos existenciales puede permitirle realizar cierres que comparten el mismo estado oculto que usted hubiera puesto en la parte existencial de un objeto.
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 específicamente el lenguaje-agnóstico, entonces 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 universal y existencialmente se puede caracterizar 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, quien llama a 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 "∃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 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 puede explotarse. Esta información de tipo de valor específico ha sido ''olvidada''; solo sabemos que existe.
Todos estos son buenos ejemplos, pero elijo responder un poco diferente. Recuerde de las matemáticas, eso ∀x. P (x) significa "para todas las x, puedo demostrar que P (x)". En otras palabras, es un tipo de función, me das una x y tengo un método para probarlo por ti.
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 específico P". Ahora, dado que no le damos mucha información sobre X además del hecho de que es un tipo, P no puede hacer mucho con eso, 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 | Nil P<X> = Option<X> = X | Nil , donde Nil es el tipo de punteros nulos. Podemos hacer una lista de ella: List<X> = (X, List<X>) | Nil List<X> = (X, List<X>) | Nil . Observe que el último es recursivo, los valores de la List<X> son pares donde el primer elemento es una X y el segundo elemento es una List<X> o bien es un puntero nulo.
Ahora, en matemáticas ∃x. P (x) significa "Puedo demostrar que hay una x particular tal que P (x) es verdadera". Puede haber muchas de tales x, pero para probarlo, una es suficiente. Otra forma de pensarlo es que debe existir un conjunto no vacío de pares de pruebas y pruebas {(x, P (x))}.
Traducido a la teoría de tipos: un tipo en la familia ∃XP<X> es un tipo X y un tipo correspondiente P<X> . Fíjate que mientras antes dábamos X a P (de modo que sabíamos todo sobre X pero P muy poco) que ahora todo lo contrario es cierto. 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 manera 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 por hurgando en P. Podría haber muchas implementaciones de este tipo, pero podría usar todos estos tipos sin importar cuál fue el elegido en particular.
Un tipo existencial es un tipo opaco.
Piensa en un manejador de archivo en Unix. Usted sabe que su tipo es int, por lo que puede forjarlo fácilmente. Por ejemplo, puede intentar leer desde el controlador 43. Si sucede que el programa tiene un archivo abierto con este identificador en particular, leerá de él. Su código no tiene que ser malicioso, simplemente descuidado (por ejemplo, el identificador podría ser una variable no inicializada).
Un tipo existencial está oculto de tu programa. Si fopen devuelve 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, el siguiente pseudocódigo se compilaría:
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 int, no es un char *, no es un archivo struct, no se puede expresar nada en el sistema de tipos. No puede declarar una variable cuyo tipo es desconocido y no puede convertir, por ejemplo, un puntero en ese tipo desconocido. El lenguaje no te deja.
Un valor de tipo existencial como ∃x. F(x) ∃x. F(x) es un par que contiene algún tipo x un valor del tipo F(x) . Mientras que un valor de tipo polimórfico como ∀x. F(x) ∀x. F(x) es una función que toma algún tipo x y produce un valor de tipo F(x) . En ambos casos, el tipo se cierra sobre algún constructor de tipo F
Tenga en cuenta que esta vista mezcla tipos y valores. La prueba existencial es un tipo y un valor. La prueba universal es una familia completa de valores indexados por tipo (o un mapeo 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 que: un valor de tipo T contiene un tipo llamado X , un valor a:X y una función f:X->int . Un productor de valores de tipo T puede elegir cualquier tipo para X y un consumidor no puede saber nada acerca de X Excepto que hay un ejemplo de esto llamado a y que este valor se puede convertir en un int dándolo a f . En otras palabras, un valor de tipo T sabe cómo producir un int alguna manera. Bueno, podríamos eliminar el tipo intermedio X y solo decir:
T = int
El universalmente cuantificado es un poco diferente.
T = ∀X { X a; int f(X); }
Esto significa: un valor de tipo T puede recibir cualquier tipo X , y producirá un valor a:X , y una función f:X->int sin importar qué X sea . En otras palabras: un consumidor de valores de tipo T puede elegir cualquier tipo para X Y un productor de valores de tipo T no puede saber nada acerca de X , pero tiene que ser capaz de producir un valor a para cualquier opción de X y poder convertir dicho valor en un int .
Obviamente, la implementación de este tipo es imposible, porque no hay ningún programa que pueda producir un valor de todos los tipos imaginables. A menos que permita absurdos como null o bottoms.
Como un existencial es un par, un argumento existencial se puede convertir a uno universal mediante currying .
(∃b. F(b)) -> Int
es lo mismo que:
∀b. (F(b) -> Int)
El primero es un rango 2 existencial. Esto lleva a la siguiente propiedad útil:
Cada tipo de rango cuantificado existencialmente
n+1es un tipo de rango universalmente cuantificadon.
Hay un algoritmo estándar para convertir los existenciales en universales, llamado Skolemization .