Экзистенциальные и универсально количественные типы в Haskell
В чем конкретно разница? Я думаю, что понимаю, как работают экзистенциальные типы, они похожи на наличие базового класса в ОО без способа понижения. Чем отличаются универсальные типы?
1 ответ
Термины "универсальный" и "экзистенциальный" здесь происходят от одноименных квантификаторов в логике предикатов.
Универсальное количественное определение обычно пишется как ∀, которое вы можете прочитать как "для всех", и примерно означает, как оно звучит: в логическом утверждении, напоминающем "∀x. ...", все, что находится вместо "..." верно для всех возможных "х", которые вы могли бы выбрать из любого набора количественных показателей.
Экзистенциальная квантификация обычно записывается как ∃, которую вы можете прочитать как "там существует", и означает, что в логическом утверждении, напоминающем "∃x. ...", все, что находится вместо "...", верно для некоторого неопределенного "х" взято из множества вещей, которые были определены количественно.
В Haskell определяемые количественно вещи являются типами (по крайней мере, игнорируя определенные языковые расширения), наши логические утверждения также являются типами, и вместо того, чтобы быть "истинными", мы думаем, что "могут быть реализованы".
Итак, универсально выраженный тип, как forall a. a -> a означает, что для любого возможного типа "а" мы можем реализовать функцию, тип которой a -> a, И действительно, мы можем:
id :: forall a. a -> a
id x = x
поскольку a В количественном выражении мы ничего не знаем об этом, и поэтому не можем проверить аргумент в любом случае. Так id является единственно возможной функцией этого типа (1).
В Haskell универсальная квантификация является "значением по умолчанию"- любые переменные типа в сигнатуре неявно универсально квантифицируются, поэтому тип id обычно написано как просто a -> a, Это также известно как параметрический полиморфизм, часто называемый просто "полиморфизмом" в Хаскеле и в некоторых других языках (например, C#), известных как "дженерики".
Экзистенциально количественный тип, такой как exists 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, который он может затем использовать с любым конкретным типом, который он выбирает.
Кроме того, хотя Хаскелл на самом деле не имеет понятия подтипирования в обычном смысле, мы можем рассматривать квантификаторы как выражение формы подтипов с иерархией, переходящей от универсальной к конкретной к экзистенциальной. Что-то типа forall a. a может быть преобразован в любой другой тип, поэтому он может рассматриваться как подтип всего; с другой стороны, любой тип может быть преобразован в тип exists a. a, делая это родительским типом всего. Конечно, первое невозможно (нет значений типа forall a. a кроме ошибок) и последнее бесполезно (вы ничего не можете сделать с типом exists a. a), но аналогия работает по крайней мере на бумаге.:]
Обратите внимание, что эквивалентность между экзистенциальным типом и универсально выраженным аргументом работает по той же причине, по которой дисперсия изменяется для входов функций.
Итак, основная идея заключается в том, что универсально количественные типы описывают вещи, которые работают одинаково для любого типа, в то время как экзистенциальные типы описывают вещи, которые работают с конкретным, но неизвестным типом.
1: Ну, не совсем - только если мы игнорируем функции, которые вызывают ошибки, такие как notId x = undefined включая функции, которые никогда не завершаются, такие как loopForever x = loopForever x,
2: Хорошо, GHC. Без расширений у Haskell есть только неявные универсальные квантификаторы и вообще нет реального способа говорить об экзистенциальных типах.
Бартош Милевски в своей книге предлагает хорошее понимание того, почему Haskell не нужен экзистенциальный квантификатор:
в псевдо-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 ....