Экзистенциальные или общечеловеческие типы в Haskell

Ответ 1

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

Универсальное квантификация обычно записывается как ∀, которую вы можете читать как "для всех", и означает примерно то, на что это похоже: в логическом выражении, напоминающем "∀ x...." все, что находится вместо "...", верно для всех возможных "x", которые вы могли бы выбрать из того, что множество вещей количественно определено.

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

В Haskell вещи, определяемые количественно, являются типами (игнорируя некоторые языковые расширения, по крайней мере), наши логические утверждения также являются типами, и вместо того, чтобы быть "истинным", мы думаем о "можно реализовать".

Таким образом, универсально квантифицированный тип типа forall a. a -> a означает, что для любого возможного типа "a" мы можем реализовать функцию, тип которой a -> a. И действительно, мы можем:

id :: forall a. a -> a
id x = x

Так как a универсально количественно, мы ничего об этом не знаем и поэтому не можем каким-либо образом оспаривать аргумент. Таким образом, id является единственно возможной функцией этого типа ⁽¹⁾.

В 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 ⁽²⁾ не имеет экзистенциальных типов напрямую (мой 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 имеет только неявные универсальные кванторы и вообще не может говорить об экзистенциальных типах.

Ответ 2

Бартош Милевски в своей книге предлагает хорошее понимание того, почему Хаскеллу не нужен экзистенциальный квантификатор:

in pseudo-Haskell:

(exists x. p x x) -> c ≅ forall x. p x x -> c

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

Следовательно, примером экзистенциально квантифицированного типа в Haskell является

data Sum = forall a. Constructor a    (i.e. forall a. (Constructor_a:: a -> Sum) ≅ Constructor:: (exists a. a) -> Sum)

который можно рассматривать как сумму data Sum = int | char | bool | .... Напротив, примером универсально определенного типа в Haskell является

data Product = Constructor (forall a. a)

который может быть как продукт data Product = int char bool ....