Что делает ключевое слово `forall` в Haskell/GHC?

Question

Я начинаю понимать, как forall Ключевое слово используется в так называемых "экзистенциальных типах", таких как:

data ShowBox = forall s. Show s => SB s

Это только подмножество того, как forall используется, и я просто не могу сосредоточиться на его использовании в таких вещах:

runST :: forall a. (forall s. ST s a) -> a

Или объясняя, почему они разные:

foo :: (forall a. a -> a) -> (Char,Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

Или весь RankNTypes материал...

Я предпочитаю ясный, свободный от жаргонного языка английский язык, а не тот язык, который является нормальным в академической среде. Большинство объяснений, которые я пытаюсь прочитать по этому поводу (те, которые я могу найти в поисковых системах), имеют следующие проблемы:

1. Они неполные. Они объясняют одну часть использования этого ключевого слова (например, "экзистенциальные типы"), что заставляет меня чувствовать себя счастливым, пока я не прочитаю код, который использует его совершенно другим способом (например, runST, foo а также bar выше).
2. Они переполнены предположениями, которые я читал последними в любой области дискретной математики, теории категорий или абстрактной алгебры, популярной на этой неделе. (Если я никогда не прочитаю слова "проконсультируйся с бумагой о деталях реализации" снова, это будет слишком рано.)
3. Они написаны способами, которые часто превращают даже простые понятия в извилистую и искаженную грамматику и семантику.

Так...

На актуальный вопрос. Кто-нибудь может полностью объяснить forall ключевое слово на чистом, простом английском языке (или, если оно где-то существует, указывает на такое ясное объяснение, которое я пропустил), которое не предполагает, что я математик, погруженный в жаргон?

---

Отредактировано, чтобы добавить:

Ниже были два выдающихся ответа из более качественных, но, к сожалению, я могу выбрать только один как лучший. Ответ Нормана был подробным и полезным, объясняя вещи таким образом, чтобы показать некоторые теоретические основы forall и в то же время показывая мне некоторые практические последствия этого. Ответ Яирчу охватил область, которую никто больше не упоминал (переменные типа scoped), и проиллюстрировал все концепции с помощью кода и сеанса GHCi. Было бы возможно выбрать оба, как лучше, я бы. К сожалению, я не могу, и, внимательно изучив оба ответа, я решил, что Яирчу слегка обходит Нормана из-за иллюстративного кода и прилагаемого объяснения. Это немного несправедливо, потому что на самом деле мне нужны были оба ответа, чтобы понять это до такой степени, что forall не оставляет меня с легким чувством страха, когда я вижу это в типовой подписи.

Answer 1

Давайте начнем с примера кода:

foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b
foob postProcess onNothin onJust mval =
    postProcess val
    where
        val :: b
        val = maybe onNothin onJust mval

Этот код не компилируется (синтаксическая ошибка) в простом Haskell 98. Для его поддержки требуется расширение forall ключевое слово.

В основном, есть 3 различных общих использования для forall ключевое слово (или, по крайней мере, так кажется), и у каждого есть свое собственное расширение Haskell: ScopedTypeVariables, RankNTypes / Rank2Types, ExistentialQuantification,

Приведенный выше код не получает синтаксическую ошибку с одним из этих включенных, но только проверки типа с ScopedTypeVariables включен.

Переменные типа Scoped:

Переменные типа Scoped помогают определить типы для кода внутри where статьи. Это делает b в val :: b тот же, что и b в foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b,

Заблуждение: вы можете услышать это, когда опускаете forall от типа это на самом деле все еще неявно там. ( из ответа Нормана: "как правило, эти языки не включают в себя полиморфные типы"). Это утверждение верно, но оно относится к другим forall а не к ScopedTypeVariables использовать.

Ранг-N-типов:

Давайте начнем с этого mayb :: b -> (a -> b) -> Maybe a -> b эквивалентно mayb :: forall a b. b -> (a -> b) -> Maybe a -> b кроме случаев, когда ScopedTypeVariables включен.

Это означает, что это работает для каждого a а также b,

Допустим, вы хотите сделать что-то подобное.

ghci> let putInList x = [x]
ghci> liftTup putInList (5, "Blah")
([5], ["Blah"])

Что должно быть типа этого liftTup? Это liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b), Чтобы понять почему, давайте попробуем закодировать это:

ghci> let liftTup liftFunc (a, b) = (liftFunc a, liftFunc b)
ghci> liftTup (\x -> [x]) (5, "Hello")
    No instance for (Num [Char])
    ...
ghci> -- huh?
ghci> :t liftTup
liftTup :: (t -> t1) -> (t, t) -> (t1, t1)

"Хм.. почему GHC делает вывод, что кортеж должен содержать два одинаковых типа? Давайте скажем, что они не должны быть"

-- test.hs
liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

ghci> :l test.hs
    Couldnt match expected type 'x' against inferred type 'b'
    ...

Хм. так что GHC не позволяет нам применять liftFunc на v так как v :: b а также liftFunc хочет x, Мы действительно хотим, чтобы наша функция получила функцию, которая принимает любые возможные x!

{-# LANGUAGE RankNTypes #-}
liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

Так что это не liftTup это работает для всех x это функция, которую он получает, которая делает.

Экзистенциальная количественная оценка:

Давайте использовать пример:

-- test.hs
{-# LANGUAGE ExistentialQuantification #-}
data EQList = forall a. EQList [a]
eqListLen :: EQList -> Int
eqListLen (EQList x) = length x

ghci> :l test.hs
ghci> eqListLen $ EQList ["Hello", "World"]
2

Чем это отличается от Rank-N-Types?

ghci> :set -XRankNTypes
ghci> length (["Hello", "World"] :: forall a. [a])
    Couldnt match expected type 'a' against inferred type '[Char]'
    ...

С рангом N-типов, forall a означало, что ваше выражение должно соответствовать всем возможным a s. Например:

ghci> length ([] :: forall a. [a])
0

Пустой список работает как список любого типа.

Так с экзистенциальной квантификацией, forall в data Определения означают, что содержащееся значение может иметь любой подходящий тип, но не все подходящие типы.

Answer 2

Кто-нибудь может полностью объяснить ключевое слово forall в ясном, простом английском языке?

Нет. (Ну, может, Дон Стюарт сможет.)

Вот барьеры для простого, ясного объяснения или forall:

• Это квантификатор. У вас должна быть хотя бы небольшая логика (исчисление предикатов), чтобы увидеть универсальный или экзистенциальный квантификатор. Если вы никогда не видели исчисление предикатов или вам не нравятся квантификаторы (и я видел во время отборочных экзаменов кандидатов, которые не устраивают), то для вас нет простого объяснения forall,

• Это квантификатор типа. Если вы еще не видели System F и не научились писать полиморфные типы, вы найдете forall сбивает с толку. Опыт работы с Haskell или ML недостаточен, потому что обычно в этих языках forall из полиморфных типов. (На мой взгляд, это ошибка дизайна языка.)

• В частности, в Хаскеле forall используется таким образом, что я нахожу запутанным. (Я не теоретик типов, но моя работа приводит меня в соприкосновение с большой теорией типов, и я вполне доволен ею.) Для меня основной источник путаницы заключается в том, что forall используется для кодирования типа, который я сам предпочел бы написать с exists, Это оправдано хитрым изоморфизмом типов, включающим квантификаторы и стрелки, и каждый раз, когда я хочу это понять, мне приходится искать вещи и самостоятельно разрабатывать изоморфизм.

  Если вас не устраивает идея изоморфизма типов или если у вас нет практики думать об изоморфизмах типов, это использование forall собирается помешать вам.

• Хотя общая концепция forall всегда одно и то же (привязка к введению переменной типа), детали различного использования могут значительно различаться. Неформальный английский не очень хороший инструмент для объяснения вариаций. Чтобы действительно понять, что происходит, вам нужна математика. В этом случае соответствующую математику можно найти во вводном тексте Бенджамина Пирса " Типы и языки программирования", который является очень хорошей книгой.

Что касается ваших конкретных примеров,

• runST должен сделать вашу голову болит. Типы высшего ранга (слева от стрелки) редко встречаются в дикой природе. Я рекомендую вам прочитать статью, которая представила runST: "Ленивые потоки функционального состояния". Это действительно хорошая статья, и она даст вам гораздо лучшую интуицию для типа runST в частности и для типов более высокого ранга в целом. Объяснение занимает несколько страниц, оно очень хорошо сделано, и я не собираюсь здесь его сокращать.

• Рассматривать

  foo :: (forall a. a -> a) -> (Char,Bool)
  bar :: forall a. ((a -> a) -> (Char, Bool))
  

  Если я позвоню barЯ могу просто выбрать любой тип a что мне нравится, и я могу передать ему функцию от типа a печатать a, Например, я могу передать функцию (+1) или функция reverse, Вы можете думать о forall как сказать "Я могу выбрать тип сейчас". (Техническое слово для выбора типа является экземпляром.)

  Ограничения на звонки foo гораздо более строгие: аргумент foo должна быть полиморфной функцией. С этим типом единственные функции, которые я могу передать foo являются id или функция, которая всегда расходится или ошибки, как undefined, Причина в том, что с foo, forall слева от стрелки, так что вызывающий foo Я не могу выбрать что a скорее - это реализация foo что выбирает что a является. Так как forall слева от стрелки, а не над стрелкой, как в barинстанцирование происходит в теле функции, а не в месте вызова.

Резюме: полное объяснение forall Ключевое слово требует математики и может быть понято только тем, кто изучал математику. Даже частичные объяснения трудно понять без математики. Но, возможно, мои частичные, не математические объяснения немного помогут. Читайте Лончбери и Пейтон Джонс runST!

---

Приложение: Жаргон "вверху", "внизу", "слева от". Они не имеют ничего общего с текстовыми способами написания типов и не имеют ничего общего с деревьями абстрактного синтаксиса. В абстрактном синтаксисе forall принимает имя переменной типа, а затем появляется полный тип "под". Стрелка принимает два типа (аргумент и тип результата) и формирует новый тип (тип функции). Тип аргумента - "слева от" стрелки; это левый дочерний элемент стрелки в дереве абстрактного синтаксиса.

Примеры:

• В forall a . [a] -> [a]поле находится над стрелкой; что слева от стрелки [a],

• В

  forall n f e x . (forall e x . n e x -> f -> Fact x f) 
                -> Block n e x -> f -> Fact x f
  

  тип в скобках будет называться "поле слева от стрелки". (Я использую такие типы в оптимизаторе, над которым я работаю.)

Answer 3

Мой оригинальный ответ:

Кто-нибудь может полностью объяснить ключевое слово forall в ясном, простом английском

Как указывает Норман, очень трудно дать ясное, ясное английское объяснение технического термина из теории типов. Мы все пытаемся все же.

Есть только одна вещь, которую нужно помнить о "forall": он привязывает типы к некоторой области видимости. Как только вы это понимаете, все довольно просто. Это эквивалент "лямбды" (или формы "пусть") на уровне типов - Норман Рэмси использует понятие "слева"/"выше", чтобы передать эту же концепцию объема в своем превосходном ответе.

Большинство вариантов использования "forall" очень просты, и вы можете найти их в Руководстве пользователя GHC, S7.8., В частности, в превосходном S7.8.5 для вложенных форм "forall".

В Haskell мы обычно оставляем связыватель для типов, когда тип определяется количественно, например:

length :: forall a. [a] -> Int

эквивалентно:

length :: [a] -> Int

Вот и все.

Поскольку теперь вы можете привязать переменные типа к некоторой области видимости, у вас могут быть области, отличные от верхнего уровня (" универсально измеренный"), как в первом примере, где переменная типа видна только в структуре данных. Это позволяет скрытые типы (" экзистенциальные типы"). Или мы можем иметь произвольную вложенность привязок ("ранг N типов").

Чтобы глубоко понять системы типов, вам нужно выучить некоторый жаргон. Это природа информатики. Тем не менее, простое использование, как и выше, должно быть в состоянии понять интуитивно, по аналогии с "let" на уровне значения. Отличное введение - Лончбери и Пейтон Джонс.

Answer 4

Вот быстрое и грязное объяснение в простых выражениях, с которым вы, вероятно, уже знакомы.

forall Ключевое слово действительно используется только одним способом в Haskell. Это всегда означает одно и то же, когда вы видите это.

Универсальное количественное определение

Универсально выраженный тип - это тип формы forall a. f a, Значение этого типа можно рассматривать как функцию, которая принимает тип a в качестве аргумента и возвращает значение типа f a, За исключением того, что в Haskell эти аргументы типа неявно передаются системой типов. Эта "функция" должна давать вам одно и то же значение независимо от того, какой тип она получает, поэтому значение является полиморфным.

Например, рассмотрим тип forall a. [a], Значение этого типа принимает другой тип a и возвращает вам список элементов того же типа a, Конечно, есть только одна возможная реализация. Это должно было бы дать вам пустой список, потому что a может быть абсолютно любого типа. Пустой список - это единственное значение списка, которое является полиморфным по своему типу элемента (так как у него нет элементов).

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

Экзистенциальное количественное определение

Экзистенциально квантованный тип будет иметь вид exists a. f a, если Haskell поддерживает эту запись. Значение этого типа можно рассматривать как пару (или "продукт"), состоящую из типа a и значение типа f a,

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

ОК, подожди минутку. Почему Haskell использует forall обозначить "экзистенциальный" тип, подобный следующему?

data ShowBox = forall s. Show s => SB s

Это может сбивать с толку, но это действительно описывает тип конструктора данных SB:

SB :: forall s. Show s => s -> ShowBox

После создания вы можете придумать значение типа ShowBox как состоящий из двух вещей. Это тип s вместе со значением типа s, Другими словами, это значение экзистенциально квантифицированного типа. ShowBox действительно может быть написано как exists s. Show s => s, если Haskell поддерживает эту запись.

runSTи друзья

Учитывая это, как они отличаются?

foo :: (forall a. a -> a) -> (Char,Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

Давайте сначала возьмем bar, Требуется тип a и функция типа a -> aи выдает значение типа (Char, Bool), Мы могли бы выбрать Int как a и дать ему функцию типа Int -> Int например. Но foo это отличается. Это требует, чтобы реализация foo быть в состоянии передать любой тип, который он хочет, функции, которую мы ему даем. Таким образом, единственная функция, которую мы могли бы дать, это id,

Теперь мы должны иметь возможность решать значение типа runST:

runST :: forall a. (forall s. ST s a) -> a

Так runST должен быть в состоянии произвести значение типа aнезависимо от того, какой тип мы даем как a, Для этого нужен аргумент типа forall s. ST s a который под капотом является просто функцией типа forall s. s -> (a, s), Эта функция должна быть в состоянии произвести значение типа (a, s) независимо от того, какой тип реализации runST решает дать как s,

Хорошо, и что? Преимущество состоит в том, что это накладывает ограничение на абонента runST в том виде a не может включать тип s совсем. Вы не можете передать ему значение типа ST s [s], например. На практике это означает, что реализация runST свободен выполнять мутацию со значением типа s, Система типов гарантирует, что эта мутация является локальной для реализации runST,

Тип runST является примером полиморфного типа ранга 2, потому что тип его аргумента содержит forall квантор. Тип foo выше также имеет ранг 2. Обычный полиморфный тип, такой как bar, является рангом-1, но становится рангом-2, если требуется, чтобы типы аргументов были полиморфными, со своими собственными forall квантор. И если функция принимает аргументы ранга 2, то ее тип - ранг 3 и так далее. В общем, тип, который принимает полиморфные аргументы ранга n имеет звание n + 1,

Answer 5

Они переполнены предположениями, которые я читал последними в любой области дискретной математики, теории категорий или абстрактной алгебры, популярной на этой неделе. (Если я никогда не прочитаю слова "проконсультируйся с бумагой о деталях реализации" снова, это будет слишком рано.)

А как насчет простой логики первого порядка? forall довольно ясно в отношении универсального количественного определения, и в этом контексте термин экзистенциальный также имеет больше смысла, хотя было бы менее неловко, если бы exists ключевое слово. То, является ли квантификация эффективно универсальной или экзистенциальной, зависит от расположения квантификатора относительно того, где переменные используются по какой стороне стрелки функции, и все это немного сбивает с толку.

Так что, если это не помогает, или если вам просто не нравится символическая логика, с более функциональной точки зрения программирования вы можете рассматривать переменные типа как просто (неявные) параметры типа для функции. Функции, принимающие параметры типа в этом смысле, традиционно пишутся с использованием прописной лямбды по любой причине, которую я напишу здесь как /\,

Итак, рассмотрим id функция:

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

Мы можем переписать его как лямбду, убрав "параметр типа" из сигнатуры типа и добавив встроенные аннотации типов:

id = /\a -> (\x -> x) :: a -> a

Вот то же самое, что сделано для const:

const = /\a b -> (\x y -> x) :: a -> b -> a

Так что ваши bar функция может быть что-то вроде этого:

bar = /\a -> (\f -> ('t', True)) :: (a -> a) -> (Char, Bool)

Обратите внимание, что тип функции, данной bar как аргумент зависит от barТип параметра. Подумайте, было ли у вас что-то вроде этого:

bar2 = /\a -> (\f -> (f 't', True)) :: (a -> a) -> (Char, Bool)

Вот bar2 применяет функцию к чему-то типа Charтак давай bar2 любой тип параметра, кроме Char вызовет ошибку типа.

С другой стороны, вот что foo может выглядеть так:

foo = (\f -> (f Char 't', f Bool True))

В отличие от bar, foo на самом деле не принимает никаких параметров типа вообще! Она принимает функцию, которая сама принимает параметр типа, а затем применяет эту функцию к двум различным типам.

Поэтому, когда вы видите forall в сигнатуре типа просто думайте об этом как о лямбда-выражении для сигнатур типов. Так же, как обычные лямбды, сфера forall распространяется как можно дальше вправо, вплоть до скобок, и точно так же, как переменные, связанные в регулярной лямбда, переменные типа, связанные forall находятся только в области видимости в выражении.

---

Post scriptum: Возможно, вы можете задаться вопросом - теперь, когда мы думаем о функциях, принимающих параметры типа, почему мы не можем сделать что-то более интересное с этими параметрами, чем поместить их в сигнатуру типа? Ответ в том, что мы можем!

Функция, которая помещает переменные типа вместе с меткой и возвращает новый тип, является конструктором типа, который можно написать примерно так:

Either = /\a b -> ...

Но нам понадобятся совершенно новые обозначения, потому что способ написания такого типа, как Either a b, уже наводит на мысль о "применить функцию Either к этим параметрам ".

С другой стороны, функция, которая как бы "соответствует шаблону" по параметрам своего типа и возвращает разные значения для разных типов, является методом класса типов. Небольшое расширение моего /\ Синтаксис выше предполагает что-то вроде этого:

fmap = /\ f a b -> case f of
    Maybe -> (\g x -> case x of
        Just y -> Just b g y
        Nothing -> Nothing b) :: (a -> b) -> Maybe a -> Maybe b
    [] -> (\g x -> case x of
        (y:ys) -> g y : fmap [] a b g ys 
        []     -> [] b) :: (a -> b) -> [a] -> [b]

Лично я думаю, что предпочитаю фактический синтаксис Haskell...

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

Answer 6

Кто-нибудь может полностью объяснить ключевое слово forall на ясном, простом английском языке (или, если оно где-то существует, указать на такое ясное объяснение, которое я пропустил), которое не предполагает, что я математик, погруженный в жаргон?

Я собираюсь попытаться объяснить только смысл и, возможно, применение forall в контексте Haskell и его систем типов.

Но прежде чем вы поймете, что я хотел бы направить вас к очень доступной и приятной беседе Рунара Бьярнасона под названием " Освобождение от ограничений, ограничение свобод". Доклад полон примеров из реальных случаев использования, а также примеров в Scala в поддержку этого утверждения, хотя он не упоминает forall, Я постараюсь объяснить forall перспектива ниже.

                CONSTRAINTS LIBERATE, LIBERTIES CONSTRAIN

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

Теперь очень распространенный пример, показывающий выразительность системы типов Haskell, - это сигнатура типа:

foo :: a -> a

Говорят, что с учетом этой сигнатуры типа существует только одна функция, которая может удовлетворить этот тип, и это identity функция или что более известно id,

На начальных этапах изучения Хаскелла я всегда интересовался следующими функциями:

foo 5 = 6

foo True = False

они оба удовлетворяют вышеуказанной сигнатуре типа, тогда почему люди из Haskell утверждают, что это id один, который удовлетворяет сигнатуре типа?

Это потому, что есть неявное forall скрыто в подписи типа. Фактический тип:

id :: forall a. a -> a

Итак, теперь давайте вернемся к утверждению: ограничения освобождают, ограничения свободы

Переводя это в систему типов, это утверждение становится:

Ограничение на уровне типа становится свободой на уровне термина

а также

Свобода на уровне типа становится ограничением на уровне термина

---

Попробуем доказать первое утверждение:

Ограничение на уровне типа.

Таким образом, наложение ограничения на нашу подпись типа

foo :: (Num a) => a -> a

становится свободой на уровне термина дает нам свободу или гибкость, чтобы написать все эти

foo 5 = 6
foo 4 = 2
foo 7 = 9
...

То же самое можно наблюдать, ограничивая a с любым другим типом класса и т. д.

Итак, что это за тип подписи: foo :: (Num a) => a -> a переводится как

∃a , st a -> a, ∀a ∈ Num

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

Следовательно, мы можем видеть добавление ограничения (что a должен принадлежать к набору Numbers), освобождает термин level для нескольких возможных реализаций.

---

Теперь перейдем ко второму утверждению и тому, которое на самом деле несет в себе объяснение forall:

Свобода на уровне типа становится ограничением на уровне термина

Итак, теперь давайте освободим функцию на уровне типа:

foo :: forall a. a -> a

Теперь это переводится как:

∀a , a -> a

Это означает, что реализация этой сигнатуры типа должна быть такой, чтобы a -> a для всех обстоятельств.

Так что теперь это начинает ограничивать нас на уровне термина. Мы больше не можем писать

foo 5 = 7

потому что эта реализация не будет удовлетворять, если мы положим a как Bool, a может быть Char или [Char] или пользовательский тип данных. При любых обстоятельствах он должен возвращать что-то похожего типа. Эта свобода на уровне типов - это то, что известно как Универсальное Количественное определение, и единственная функция, которая может удовлетворить это

foo a = a

который обычно известен как identity функция

---

следовательно forall это liberty на уровне типа, фактическая цель которого состоит в constrain термин уровень для конкретной реализации.

Answer 7

Причина, по которой это ключевое слово используется по-разному, заключается в том, что оно фактически используется как минимум в двух разных системных расширениях: типах более высокого ранга и экзистенциалах.

Вероятно, лучше просто прочитать и понять эти две вещи отдельно, а не пытаться получить объяснение того, почему "forall" является подходящим синтаксисом в обоих случаях одновременно.

Answer 8

Как экзистенциально экзистенциально?

С экзистенциальной квантификацией, forallв data Определения означают, что содержащееся значение может иметь любой подходящий тип, но не все подходящие типы. - ответ Ячиру

Объяснение почемуforallвdataопределения изоморфны (exists a. a) (псевдо-Haskell) можно найти в "Хаскеле / ​​Экзистенциально квантифицированные типы" в wikibooks.

Ниже приводится краткое стенографическое резюме:

data T = forall a. MkT a -- an existential datatype
MkT :: forall a. a -> T -- the type of the existential constructor

Когда сопоставление с образцом / деконструкция MkT xкакой тип x?

foo (MkT x) = ... -- -- what is the type of x?

x может быть любого типа (как указано в forall) и так это тип:

x :: exists a. a -- (pseudo-Haskell)

Следовательно, следующие изоморфны:

data T = forall a. MkT a -- an existential datatype
data T = MkT (exists a. a) -- (pseudo-Haskell)

Форалл означает Форалл

Моя простая интерпретация всего этого заключается в том, что "forall на самом деле означает "для всех". Важное различие, которое нужно сделать, это влияние forall на определение по сравнению с применением функции.

forall означает, что определение значения или функции должно быть полиморфным.

Если определяемая вещь является полиморфным значением, то это означает, что значение должно быть действительным для всех подходящих a, что довольно ограничительно.

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

Если forall находится внутри типа параметра функции (т.е. Rank2Type) тогда это означает, что применяемый параметр должен быть по- настоящему полиморфным, чтобы соответствовать идее forall означает, что определение полиморфно. В этом случае тип параметра может быть выбран более одного раза в определении функции ( "и выбирается реализацией функции", как указано Норманом)

Поэтому причина существования data определения позволяет любому a это потому, что конструктор данных является полиморфной функцией:

MkT :: forall a. a -> T

вид MkT:: a -> *

Что означает любой a может применяться к функции. В противоположность, скажем, полиморфному значению:

valueT :: forall a. [a]

вид значения T:: a

Это означает, что определение valueT должно быть полиморфным. В этом случае, valueT можно определить как пустой список [] всех типов.

[] :: [t]

Различия

Хотя значение для forall соответствует в ExistentialQuantification а также RankNTypeэкзистенциал имеет разницу, так как data Конструктор может быть использован в сопоставлении с образцом. Как описано в руководстве пользователя GHC:

При сопоставлении с образцом каждое сопоставление с образцом вводит новый, отдельный тип для каждой переменной экзистенциального типа. Эти типы не могут быть объединены с любым другим типом, и при этом они не могут выходить из области соответствия шаблона.