Ответ 1
Заголовок и теги должны адекватно объяснить вопрос.
Эрр, не совсем. Вы использовали тег 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]? Мы знаем, что типы, содержащие ∀, исходят из членов, содержащих Λ:
term1 :: ∀a. [a]
term1 = Λa. ?
Внутри тела, отмеченного ?, мы должны указать термин типа [a]. То есть термин типа ∀a. [a] означает "с учетом любого типа a, я дам вам список типов [a]".
Однако мы ничего не знаем о a, так как это аргумент, переданный извне. Таким образом, мы можем вернуть пустой список
term1 = Λa. []
или undefined значение
term1 = Λa. undefined
или список, содержащий только undefined значения
term1 = Λa. [undefined, undefined]
но не намного больше.
[∀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
Экзистенциальные типы
Значение универсального (∀) типа - это функция от типов к значениям. Значение типа existential (∃) - это пара типа и значения.
Более конкретно: значение типа
∃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
Дальнейшее чтение
Для введения в теорию я настоятельно рекомендую Типы и языки программирования от Pierce. Для обсуждения экзистенциальных типов в GHC см. руководство GHC и Haskell wiki.