Заголовок и теги должны адекватно объяснить вопрос.
Ошибка, не совсем.Вы использовали тег existential-type, но ни один из указанных вами типов не является экзистенциальным.
Система F
Здесь уже есть несколько хороших ответов, поэтому я воспользуюсь другим подходом и будунемного более формально.Полиморфные значения, по сути, являются функциями типов, но синтаксис Haskell оставляет неявными как типовые абстракции, так и приложения типов, что скрывает проблему.Мы будем использовать обозначение System F , которое имеет явную абстракцию типа и приложение типа.
Например, знакомая функция map будет написана
map :: ∀a. ∀b. (a → b) → [a] → [b]
map = Λa. Λb. λ(f :: a → b). λ(xs :: [a]). case xs of
[] → []
(y:ys) → f y : map @a @b f ys
map теперь является функцией четырех аргументов: двух типов (a и b), функции и списка.Мы пишем функцию над типами, используя Λ (лямбда в верхнем регистре), и функцию над значениями, как обычно, используя λ.Термин, содержащий Λ, порождает тип, содержащий ∀, так же как термин, содержащий λ, порождает тип, содержащий →.Я использую нотацию @a (как в GHC Core) для обозначения применения аргумента типа.
Таким образом, значение полиморфного типа похоже на функцию от типов к значениям.Вызывающий полиморфную функцию получает возможность выбрать аргумент типа, и функция должна соответствовать.
∀a.[a]
Как тогда мы напишем термин типа ∀a. [a]?Мы знаем, что типы, содержащие ∀, взяты из терминов, содержащих Λ:
term1 :: ∀a. [a]
term1 = Λa. ?
В теле, отмеченном ?, мы должны предоставить термин типа [a].То есть термин типа ∀a. [a] означает «для любого типа a, я дам вам список типа [a]».
Однако мы не знаем ничего конкретного о a, посколькуэто аргумент, переданный извне.Таким образом, мы можем вернуть пустой список
term1 = Λa. []
или неопределенное значение
term1 = Λa. undefined
или список, содержащий только неопределенные значения
term1 = Λa. [undefined, undefined]
, но не более того.
[∀a.a]
А как же [∀a. a], тогда?Если ∀ обозначает функцию для типов, тогда [∀a. a] - это список функций.Мы можем предоставить столько, сколько захотим:
term2 :: [∀a. a]
term2 = []
или столько:
term2 = [f, g, h]
Но каковы наши варианты выбора f, g и h?
f :: ∀a. a
f = Λa. ?
Теперь мы хорошо и действительно застряли.Мы должны предоставить значение типа a, но мы ничего не знаем о типе a.Так что наш единственный выбор -
f = Λa. undefined
Так что наши опции для term2 выглядят как
term2 :: [∀a. a]
term2 = []
term2 = [Λa. undefined]
term2 = [Λa. undefined, Λa. undefined]
и т. Д.И давайте не будем забывать
term2 = undefined
Экзистенциальные типы
Значение универсального (∀) типа - это функция от типов к значениям.Значением экзистенциального (∃) типа является пара типа и значения.
Более конкретно: значение типа
∃x. T
представляет собой пару
(S, v)
где S - это тип, а где v :: T, если вы связываете переменную типа x с S в T.
Вот сигнатура экзистенциального типа инесколько терминов с этим типом:
term3 :: ∃a. a
term3 = (Int, 3)
term3 = (Char, 'x')
term3 = (∀a. a → Int, Λa. λ(x::a). 4)
Другими словами, мы можем поместить любое значение, которое нам нравится, в ∃a. a, пока мы соединяем это значение с его типом.
пользователь значения типа ∀a. a находится в отличном положении;они могут выбрать любой конкретный тип, который им нравится, используя приложение типа @T, чтобы получить термин типа T. производитель значения типа ∀a. a находится в ужасном положении: они должны быть готовы к созданию любого запрашиваемого типа, поэтому (как и в предыдущем разделе) единственный выбор - Λa. undefined.
Пользователь значения типа ∃a. a находится в ужасном положении;значение внутри имеет некоторый неизвестный специфический тип, а не гибкое полиморфное значение. продюсер значения типа ∃a. a находится в отличном положении;они могут вставить в пару любое значение, которое им нравится, как мы видели выше.
Так что же является менее бесполезным экзистенциальным?Как насчет значений в паре с бинарной операцией:
type Something = ∃a. (a, a → a → a, a → String)
term4_a, term4_b :: Something
term4_a = (Int, (1, (+) @Int , show @Int))
term4_b = (String, ("foo", (++) @Char, λ(x::String). x))
Использование:
triple :: Something → String
triple = λ(a, (x :: a, f :: a→a→a, out :: a→String)).
out (f (f x x) x)
Результат:
triple term4_a ⇒ "3"
triple term4_b ⇒ "foofoofoo"
Мы упаковалидо типа и некоторые операции над этим типом.Пользователь может применить наши операции, но не может проверить конкретное значение - мы не можем сопоставить шаблон с x в пределах triple, так как его тип (следовательно, набор конструкторов) неизвестен.Это больше похоже на объектно-ориентированное программирование.
Использование экзистенциалов для реального
Прямой синтаксис для экзистенциалов, использующих пары ∃ и тип-значение, был бы весьма удобен. UHC частично поддерживает этот прямой синтаксис.Но GHC не делает.Чтобы ввести экзистенциалы в GHC, нам нужно определить новые типы «оболочек».
Перевод приведенного выше примера:
{-# LANGUAGE ExistentialQuantification #-}
data Something = forall a. MkThing a (a -> a -> a) (a -> String)
term_a, term_b :: Something
term_a = MkThing 1 (+) show
term_b = MkThing "foo" (++) id
triple :: Something -> String
triple (MkThing x f out) =
out (f (f x x) x)
Есть пара отличий от нашего теоретического подхода.Тип приложения, абстракция типа и пары типов снова являются неявными.Кроме того, обертка запутанно написана с forall, а не exists.Это ссылается на тот факт, что мы объявляем экзистенциальный тип, но конструктор данных имеет универсальный тип:
MkThing :: forall a. a -> (a -> a -> a) -> (a -> String) -> Something
Часто,мы используем экзистенциальную квантификацию для «захвата» ограничения класса типов.Мы могли бы сделать что-то подобное здесь:
data SomeMonoid = forall a. (Monoid a, Show a) => MkMonoid a
Дальнейшее чтение
Для введения в теорию я настоятельно рекомендую Типы и языки программирования Пирс.Для обсуждения экзистенциальных типов в GHC см. руководство по GHC и вики Haskell .