В чем разница между forall a. [a] и [forall a. а]?

Ответ 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.

Ответ 2

Тип forall a. [a] означает, что для любого отдельного типа это список, содержащий этот тип. Это также означает, что просто [a] означает и является типом [], пустым конструктором данных списка.

Тип [forall a. a] означает, что у вас есть список значений с полиморфным типом, то есть каждый из них является значением любого возможного типа, не обязательно таким же, как и другие элементы списка. Никакое возможное значение не может иметь тип forall a. a, поэтому это также должен быть пустой список.

Разница заключается в том, что, хотя первый может быть использован как список любого типа (по определению, в основном), последний не может быть использован как список какого-либо конкретного типа вообще, поскольку нет способа чтобы привязать его к любому типу.

Для обращения к тегу - экзистенциальный тип - это тот, который в пределах некоторой области будет создан каким-то неизвестным конкретным типом. Это может быть что угодно, поэтому оно представлено чем-то вроде forall a. a выше. Чтобы убедиться, что что-либо с экзистенциальным типом используется только в пределах области, где будет доступен фактический тип, компилятор не позволяет экзистенциальным типам "экранировать".

Это может помочь думать о кванторе forall как о выражении лямбда - он вводит новую переменную типа и связывает этот идентификатор в некоторой области. Вне этой области идентификатор не имеет значения, поэтому forall a. a довольно бесполезен.

Ответ 3

При использовании для типов forall означает пересечение. Итак, forall a. a - это пересечение всех типов или что-то вроде Int ∩ String ∩ ..., которое, кажется, дает пустое множество, но каждый тип имеет дополнительный элемент, называемый bottom или ⊥ или undefined в Haskell. Отсюда получаем, что forall a. a = {⊥}. Фактически мы можем определить тип, содержащий только нижний:

data Zero

После этой настройки мы рассмотрим наши типы, начиная с [forall a. a]. Он определяет список нижних частей или [Zero], в котором есть элементы [], [undefined], [undefined, undefined], .... Давайте проверим его в ghci:

> let l = [undefined, undefined]::[Zero]
> :t l
l :: [Zero]

Аналогичным образом forall a. [a] является пересечением всех типов списка, а так как ∩[a] = [∩a] это снова [Zero].

Чтобы выполнить окончательную проверку, определите:

type L = forall a. [a]
type U = [forall a. a]

и в ghci:

> let l2 = [undefined, undefined]::L
> let l3 = [undefined, undefined]::U
> :t l2
l2 :: [a]
> :t l3
l3 :: U

Обратите внимание, что l2::[a] объясняется, что Haskell помещает неявный forall перед всеми полиморфными типами.