Ответ 1
Термины "универсальный" и "экзистенциальный" здесь исходят от так называемых кванторов в предикатной логике.
Универсальное квантификация обычно записывается как ∀, которую вы можете читать как "для всех", и означает примерно то, на что это похоже: в логическом выражении, напоминающем "∀ x...." все, что находится вместо "...", верно для всех возможных "x", которые вы могли бы выбрать из того, что множество вещей количественно определено.
Экзистенциальная квантификация обычно записывается как ∃, которую вы можете читать как "существует", и означает, что в логическом выражении, напоминающем "∃x...." все, что находится вместо "...", верно для некоторого неуказанного "x", взятого из множества вещей, количественно оцененных.
В Haskell вещи, определяемые количественно, являются типами (игнорируя некоторые языковые расширения, по крайней мере), наши логические утверждения также являются типами, и вместо того, чтобы быть "истинным", мы думаем о "можно реализовать".
Таким образом, универсально квантифицированный тип типа forall a. a -> a означает, что для любого возможного типа "a" мы можем реализовать функцию, тип которой a -> a. И действительно, мы можем:
id :: forall a. a -> a
id x = x
Так как a универсально количественно, мы ничего об этом не знаем и поэтому не можем каким-либо образом оспаривать аргумент. Таким образом, id является единственно возможной функцией этого типа (1).
В Haskell универсальное квантификация - это значение по умолчанию - переменные любого типа в подписи неявно универсально количественно, поэтому тип id обычно записывается как просто a -> a. Это также называется параметрическим полиморфизмом, часто называемым "полиморфизмом" в Haskell, а также на некоторых других языках (например, С#), известных как "generics".
Цитированный по экзистенциальному типу тип, такой как exists a. a -> a, означает, что для некоторого определенного типа "a" мы можем реализовать функцию, тип которой a -> a. Любая функция будет делать, поэтому я выберу один из них:
func :: exists a. a -> a
func True = False
func False = True
... который, конечно, является "не" функцией на буле. Но улов в том, что мы не можем использовать его как таковое, потому что все, что мы знаем о типе "а", это то, что оно существует. Любая информация о том, какой тип она может быть, была отброшена, что означает, что мы не можем применять func к любым значениям.
Это не очень полезно.
Итак, что мы можем сделать с func? Ну, мы знаем, что это функция с одним и тем же типом для ввода и вывода, поэтому мы могли бы составить ее с собой, например. По сути, единственное, что вы можете сделать с чем-то, что имеет экзистенциальный тип, - это то, что вы можете сделать на основе несуществующих частей этого типа. Точно так же, учитывая что-то типа exists a. [a], мы можем найти его длину или объединить его в себя или удалить некоторые элементы или что-то еще, что мы можем сделать с любым списком.
Этот последний бит возвращает нас к универсальным квантизаторам, и причина, по которой Haskell (2) не имеет экзистенциальных типов напрямую (мой exists выше полностью фиктивный, увы): поскольку вещи с экзистенциально квантованными типами могут использоваться только с операциями, которые имеют универсально квантифицированные типы, мы можем написать тип exists a. a как forall r. (forall a. a -> r) -> r - другими словами, для всех типов результатов r, учитывая функцию, которая для всех типов a принимает аргумент типа a и возвращает значение типа r, мы можем получить результат типа r.
Если вам непонятно, почему они почти эквивалентны, обратите внимание на то, что общий тип не оценивается в целом для a - скорее, он принимает аргумент, который сам по себе количественно оценивается для a, который он может затем использовать с любым конкретным типом, который он выбирает.
В стороне, в то время как у Haskell на самом деле нет понятия подтипирования в обычном смысле, мы можем рассматривать кванторы как выражение формы подтипирования, причем иерархия переходит от универсального к конкретному к экзистенциальному. Кое-что типа forall a. a может быть преобразовано в любой другой тип, поэтому его можно рассматривать как подтип всего; с другой стороны, любой тип может быть преобразован в тип exists a. a, что делает родительский тип всего. Конечно, первое невозможно (нет значений типа forall a. a кроме ошибок), а последнее бесполезно (вы ничего не можете сделать с типом exists a. a), но аналогия работает на бумаге как минимум.:]
Обратите внимание, что эквивалентность между экзистенциальным типом и универсальным квантованным аргументом работает по той же причине, что variance переворачивается для ввода функций.
Итак, основная идея примерно в том, что универсально квантифицированные типы описывают вещи, которые работают одинаково для любого типа, тогда как экзистенциальные типы описывают вещи, которые работают с определенным, но неизвестным типом.
1: Ну, не совсем - только если мы игнорируем функции, вызывающие ошибки, такие как notId x = undefined, включая функции, которые никогда не заканчиваются, например loopForever x = loopForever x.
2: Ну, GHC. Без расширений Haskell имеет только неявные универсальные кванторы и вообще не может говорить об экзистенциальных типах.