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

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

См.:

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

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

Поскольку я понимаю, что это - математика способ описать интерфейсы/абстрактный класс.

Что касается T = в€ѓX {X a; интервал f (X);}

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

abstract class MyType<T>{
    private T a;

    public abstract int f(T x);
}

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

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

Подумайте о дескрипторе файла в 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 * , а не структура File - ничего, что вы можете выразить в системе типов. Вы не можете объявить переменную, тип которой неизвестен, и вы не можете привести, скажем, указатель к этому неизвестному типу. Язык вам не позволит.