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

Когда кто-то определяет универсальный тип ∀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 (например, 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);
   }
}

Значение экзистенциального типа, например ∃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 или низа.

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

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

такой же как:

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

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

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

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

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

Я не могу ответить на все подробности о экзистенциальных типах (например, дать точное определение, перечислить все возможные варианты использования, их отношение к абстрактным типам данных и т. Д.), Потому что я просто недостаточно осведомлен для этого. Я продемонстрирую (используя 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;
}

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

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

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

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

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

Наиболее очевидное исправление - просто сделать height универсальным, добавив параметр типа α в его сигнатуру:

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

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

2. Решение экзистенциального типа:

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

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

Все это хорошие примеры, но я предпочитаю отвечать на них немного иначе. Напомним из математики, что ∀x. P (x) означает «для всех x я могу доказать, что P (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. Хотя у нас нет возможности напрямую манипулировать им, мы можем наблюдать его эффект, тыкает в P. Может быть много реализаций этого типа, но вы можете использовать все эти типы независимо от того, какой именно из них был выбран.

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

С универсальным типом использование 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 (или выполнять любые операции, предусмотренные внутри структуры данных) по запросу.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

trait Existential {
  type Parameter <: Interface
}

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

trait Existential[Parameter <: Interface]

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

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

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

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

Видеть:

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

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

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

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

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

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

abstract class MyType<T>{
    private T a;

    public abstract int f(T x);
}

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