Что такое экзистенциальный тип?

Ответ 1

Когда кто-то определяет универсальный тип ∀X, они говорят: вы можете подключить любой тип, который вам нужен, мне не нужно ничего знать о типе, чтобы выполнять свою работу, я буду ссылаться только на него непрозрачно как X.

Когда кто-то определяет экзистенциальный тип ∃X, они говорят: я буду использовать любой тип, который я хочу здесь; вы не знаете ничего о типе, поэтому вы можете относиться к нему только как X.

Универсальные типы позволяют писать такие вещи, как:

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

Функция copy не имеет понятия, что T будет на самом деле, но это не нужно.

Экзистенциальные типы позволят вам писать такие вещи, как:

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);
   }
}

Каждая реализация виртуальной машины в списке может иметь другой тип байт-кода. Функция runAllCompilers не знает, что такое тип байт-кода, но это не нужно; все, что он делает, это передать байт-код от VirtualMachine.compile до VirtualMachine.run.

Шаблоны типов Java (ex: List<?>) - очень ограниченная форма экзистенциальных типов.

Обновление:. Забыл упомянуть, что вы можете сортировать типы экзистенциальных типов с универсальными типами. Сначала сверните свой универсальный тип, чтобы скрыть параметр типа. Во-вторых, инвертируйте управление (это эффективно меняет части "вы" и "я" в приведенных выше определениях, что является основным различием между экзистенциальными и универсальными).

// 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);
}

Теперь мы можем вызвать VMWrapper наш собственный VMHandler, который имеет универсальную функцию handle. Чистый эффект тот же, наш код должен рассматривать B как непрозрачный.

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);
         }
      });
   }
}

Пример реализации виртуальной машины:

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);
   }
}

Ответ 2

Значение экзистенциального типа, например ∃x. F(x) , представляет собой пару, содержащую некоторый тип x и значение типа F(x). В то время как значение полиморфного типа типа ∀x. F(x) является функцией, которая принимает некоторый тип x и выдает значение типа F(x). В обоих случаях тип закрывается над некоторым конструктором типа F.

Обратите внимание, что это представление смешивает типы и значения. Экзистенциальное доказательство - это один тип и одно значение. Универсальное доказательство - это целое семейство значений, индексированных по типу (или отображению от типов к значениям).

Таким образом, разница между двумя указанными вами типами выглядит следующим образом:

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

Это означает: значение типа T содержит тип x, значение a:X и функцию f:X->int. Производитель значений типа T выбирает любой тип для x, и потребитель ничего не знает о x. За исключением того, что один пример из него называется a и что это значение можно превратить в int, указав его на F. Другими словами, значение типа T знает, как создать int каким-то образом. Ну, мы могли бы исключить промежуточный тип x и просто сказать:

T = int

Универсально определенная единица немного отличается.

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

Это означает: значение типа T может быть задано любым типом x, и оно будет выдавать значение a:X, а функция f:X->int независимо от того, что x. Другими словами: потребитель значений типа T может выбрать любой тип для x. И производитель значений типа T вообще ничего не знает о x, но он должен иметь возможность создавать значение a для любого выбора x и иметь возможность превратить такой значение в int.

Очевидно, что реализация этого типа невозможна, потому что нет никакой программы, которая может генерировать значение любого воображаемого типа. Если вы не допускаете абсурд, например, null или днища.

Поскольку существует экзистенциальная пара, экзистенциальный аргумент может быть преобразован в универсальный с помощью currying.

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

совпадает с:

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

Первый является экзистенциальным rank-2. Это приводит к следующему полезному свойству:

Каждый экзистенциально квантованный тип ранга n+1 является универсально квантованным типом ранга n.

Существует стандартный алгоритм для превращения экзистенциальных объектов в универсальности, называемый Skolemization.

Ответ 3

Я думаю, что имеет смысл объяснять экзистенциальные типы вместе с универсальными типами, поскольку эти два понятия дополняют друг друга, т.е. один является "противоположным" другим.

Я не могу ответить на каждую деталь о экзистенциальных типах (например, дать точное определение, перечислить все возможные применения, их отношение к абстрактным типам данных и т.д.), потому что я просто недостаточно осведомлен об этом. Я продемонстрирую только (используя Java), что эта статья HaskellWiki утверждает, что это главный эффект экзистенциальных типов:

Экзистенциальные типы могут использоваться для различных целей. Но то, что они делают, это "скрыть" переменную типа с правой стороны. Как правило, любая переменная типа, появляющаяся справа, также должна появляться слева [...]

Пример настройки:

Следующий псевдокод - не совсем допустимая Java, хотя было бы достаточно легко исправить это. На самом деле, именно то, что я собираюсь сделать в этом ответе!

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

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

Позвольте мне кратко изложить это для вас. Мы определяем & hellip;

• рекурсивный тип Tree<α>, который представляет node в двоичном дереве. Каждый node хранит value некоторого типа α и имеет ссылки на необязательные подделки left и right того же типа.

• функция height, которая возвращает наибольшее расстояние от любого листа node до корня node t.

Теперь включите указанный выше псевдокод для height в правильный синтаксис Java! (Я буду продолжать пропускать некоторые шаблоны для краткости, такие как модификаторы объектной ориентации и доступности). Я собираюсь показать два возможных решения.

1. Решение универсального типа:

Самое очевидное решение состоит в том, чтобы просто сделать height generic, введя параметр типа α в свою подпись:

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

Это позволит вам объявлять переменные и создавать выражения типа α внутри этой функции, если хотите. Но...

2. Экзистенциальное решение:

Если вы посмотрите на наш метод, вы заметите, что мы на самом деле не обращаемся или не работаем с чем-либо типа α! Нет выражений, имеющих этот тип, и никаких переменных, объявленных с этим типом... так, почему мы должны вообще делать height generic? Почему мы не можем просто забыть о α? Как оказалось, мы можем:

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

Как я писал в самом начале этого ответа, экзистенциальные и универсальные типы являются взаимодополняющими/двойственными по своей природе. Таким образом, если решение универсального типа заключалось в том, чтобы сделать height более общим, тогда мы должны ожидать, что экзистенциальные типы имеют обратный эффект: сделать его менее общим, а именно, скрывая/удаляя параметр типа α.

Как следствие, вы больше не можете ссылаться на тип t.value в этом методе и не манипулировать никакими выражениями этого типа, потому что к нему не привязан идентификатор. (? подстановочный знак - это специальный токен, а не идентификатор, который "захватывает" тип.) t.value эффективно становится непрозрачным; возможно, единственное, что вы все еще можете сделать с ним, - это применить его к Object.

Резюме:

===========================================================
                     |    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   |                  
=====================+=====================================

Ответ 4

Это все хорошие примеры, но я решил ответить на него немного по-другому. Напомним из математики, что ∀x. P (x) означает "для всех x, я могу доказать, что P (x)". Другими словами, это своего рода функция, вы даете мне x, и у меня есть метод, чтобы доказать это вам.

В теории типов мы говорим не о доказательствах, а о типах. Поэтому в этом пространстве мы подразумеваем "для любого типа X, который вы даете мне, я дам вам определенный тип P". Теперь, поскольку мы не даем P много информации о X, кроме того, что это тип, P не может много сделать с этим, но есть некоторые примеры. P может создать тип "всех пар одного типа": P<X> = Pair<X, X> = (X, X). Или мы можем создать тип опции: P<X> = Option<X> = X | Nil, где Nil - тип нулевых указателей. Мы можем сделать из него список: List<X> = (X, List<X>) | Nil. Обратите внимание, что последний является рекурсивным, значения List<X> являются либо парами, где первый элемент является X, а второй - List<X>, либо он является нулевым указателем.

Теперь, в математике ∃x. P (x) означает "Я могу доказать, что существует конкретное x такое, что P (x) истинно". Их может быть много, но чтобы доказать это, этого достаточно. Другой способ подумать о том, что должен существовать непустой набор доказательно доказанных пар {(x, P (x))}.

Перевод на теорию типов: Тип в семействе ∃X.P<X> - это тип X и соответствующий тип P<X>. Обратите внимание, что пока мы не дали X P, (так что мы знали все о X, но P очень мало), что теперь все наоборот. P<X> не обещает предоставить какую-либо информацию о X, просто там есть одно и что это действительно тип.

Как это полезно? Ну, P может быть типом, который имеет способ разоблачить свой внутренний тип X. Примером может служить объект, который скрывает внутреннее представление его состояния X. Хотя мы не имеем никакого способа прямого манипулирования им, мы можем наблюдать его влияние на толкать на П. Может быть много реализаций этого типа, но вы можете использовать все эти типы независимо от того, какой именно был выбран.

Ответ 5

Экзистенциальный тип - непрозрачный.

Подумайте о дескрипторе файла в Unix. Вы знаете, что его тип int, поэтому вы можете легко подделать его. Например, вы можете попытаться прочитать из ручки 43. Если так получится, что программа открыла файл с этим конкретным дескриптором, вы прочитаете его. Ваш код не должен быть вредоносным, просто неаккуратным (например, дескриптор может быть неинициализированной переменной).

Экзистенциальный тип скрыт от вашей программы. Если fopen возвратил экзистенциальный тип, все, что вы могли бы сделать с ним, это использовать его с некоторыми библиотечными функциями, которые принимают этот экзистенциальный тип. Например, следующий псевдокод будет компилироваться:

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

Интерфейс "read" объявлен как:

Существует тип T такой, что:

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

Переменная exfile не является int, а не char*, а не структурным файлом, и вы ничего не можете выразить в системе типов. Вы не можете объявить переменную, тип которой неизвестен, и вы не можете использовать, скажем, указатель на этот неизвестный тип. Язык не позволит вам.

Ответ 6

Чтобы прямо ответить на ваш вопрос:

При использовании универсального типа использование T должно включать параметр типа X. Например T<String> или T<Integer>. Для использования в экзистенциальном типе T этот параметр типа не указан, поскольку он неизвестен или не имеет значения - просто используйте T (или в Java T<?>).

Дополнительная информация:

Универсальные/абстрактные типы и экзистенциальные типы - это двойственность перспективы между потребителем/клиентом объекта/функции и производителем/ее реализацией. Когда одна сторона видит универсальный тип, другой видит экзистенциальный тип.

В Java вы можете определить общий класс:

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();

• С точки зрения клиента MyClass, T универсален, потому что вы можете заменить любой тип для T при использовании этого класса, и вы должны знать фактический тип T, когда вы используете экземпляр MyClass
• С точки зрения методов экземпляра в MyClass, T является экзистенциальным, потому что он не знает реального типа T
• В Java ? представляет экзистенциальный тип - таким образом, когда вы находитесь внутри класса, T в основном ?. Если вы хотите обрабатывать экземпляр MyClass с помощью T экзистенциального, вы можете объявить MyClass<?>, как в приведенном выше примере secretMessage().

Экзистенциальные типы иногда используются, чтобы скрыть детали реализации чего-либо, как обсуждалось в другом месте. Версия Java может выглядеть так:

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

Немного сложно сделать это правильно, потому что я претендую на то, чтобы быть в каком-то функциональном языке программирования, которого Java нет. Но дело здесь в том, что вы захватываете какое-то состояние плюс список функций, которые работают в этом состоянии, и вы не знаете реального типа государственной части, но функции выполняются, так как они были сопоставлены с этим типом уже.

Теперь в Java все не конечные не-примитивные типы частично экзистенциальны. Это может показаться странным, но поскольку переменная, объявленная как Object, потенциально может быть подклассом Object, вы не можете объявить конкретный тип, только "этот тип или подкласс". Итак, объекты представлены как бит состояния плюс список функций, которые работают в этом состоянии - точно, какая функция для вызова определяется во время выполнения путем поиска. Это очень похоже на использование экзистенциальных типов выше, где у вас есть экзистенциальная часть состояния и функция, работающая в этом состоянии.

В статически типизированных языках программирования без подтипирования и приведения экзистенциальные типы позволяют управлять списками объектов с различной типизацией. Список T<Int> не может содержать T<Long>. Однако список T<?> может содержать любое изменение T, позволяющее вставлять в список много разных типов данных и преобразовывать их все в int (или делать какие-либо операции в структуре данных) по требованию.

Можно почти всегда конвертировать запись с экзистенциальным типом в запись без использования закрытий. Закрытие также экзистенциально типизируется тем, что свободные переменные, которые он закрывает, скрыты от вызывающего. Таким образом, язык, который поддерживает замыкания, но не экзистенциальные типы, может позволить вам делать замыкания, которые имеют одно и то же скрытое состояние, которое вы бы вложили в экзистенциальную часть объекта.

Ответ 7

Кажется, что я немного опаздываю, но в любом случае этот документ добавляет еще одно представление о том, какие существуют экзистенциальные типы, хотя это и не является специфическим для языка-агностиком, тогда должно быть довольно просто понять экзистенциальные типы: http://www.cs.uu.nl/groups/ST/Projects/ehc/ehc-book.pdf (глава 8)

Разность между универсальным и экзистенциально квантованным типом может быть охарактеризована следующим наблюдением:

• Использование значения с квантифицированным типом type определяет тип, который нужно выбрать для экземпляра переменной количественного типа. Например, вызывающий элемент функции идентификации "id:: ∀a.a → a" определяет тип для выбора переменной типа a для этого конкретного приложения id. Для приложения функции "id 3" этот тип равен Int.

• Создание значения с количественным типом type определяет и скрывает тип переменной количественного типа. Например, создатель "∃a. (A, a → Int)" мог построить значение этого типа из "(3, λx → x)"; другой создатель построил значение с тем же типом от "(x, λx → ord x)". С точки зрения пользователей оба значения имеют один и тот же тип и поэтому взаимозаменяемы. Значение имеет определенный тип, выбранный для переменной типа a, но мы не знаем, какой тип, поэтому эту информацию больше нельзя использовать. Эта информация об определенном типе значения была "забыта"; мы знаем, что он существует.

Ответ 8

Исследование абстрактных типов данных и скрытия информации приводило к появлению экзистенциальных типов в языках программирования. Создание абстрактного типа данных скрывает информацию об этом типе, поэтому клиент такого типа не может злоупотреблять им. Скажем, у вас есть ссылка на объект... некоторые языки позволяют вам ссылаться на ссылку на байты и делать все, что захотите, с той частью памяти. В целях гарантирования поведения программы полезно, чтобы язык обеспечивал, чтобы вы действовали только на ссылку на объект с помощью методов, которые предоставляет разработчик объекта. Вы знаете, что тип существует, но не более того.

См:

Абстрактные типы имеют экзистенциальный тип, MITCHEL и PLOTKIN

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

Ответ 9

Универсальный тип существует для всех значений параметра (ов) типа. Экзистенциальный тип существует только для значений параметра (ов) типа, которые удовлетворяют ограничениям экзистенциального типа.

Например, в Scala одним из способов выражения экзистенциального типа является абстрактный тип, который ограничен некоторыми верхними или нижними границами.

trait Existential {
  type Parameter <: Interface
}

Эквивалентно ограниченный универсальный тип является экзистенциальным типом, как в следующем примере.

trait Existential[Parameter <: Interface]

Любой сайт использования может использовать Interface потому что любые подтипы Existential должны определять type Parameter который должен реализовать Interface.

Вырожденный случай экзистенциального типа в Scala является абстрактным типом, который никогда не упоминается и, следовательно, не должен определяться каким-либо подтипом. Это эффективно имеет сокращенное обозначение List[_] в Scala и List<?> В Java.

Мой ответ был вдохновлен предложением Мартина Одерского объединить абстрактные и экзистенциальные типы. Сопровождающий слайд помогает понять.

Ответ 10

Я создаю эту диаграмму. не знаю, строго ли это. Но если это помогает, я рад.

Ответ 11

Как я понимаю, это математический способ описания интерфейсов/абстрактного класса.

Что касается T = ∃X {X a; int f (X); }

Для С# он переводит общий абстрактный тип:

abstract class MyType<T>{
    private T a;

    public abstract int f(T x);
}

"Экзистенциальный" означает, что существует некоторый тип, подчиняющийся правилам, определенным здесь.