Я начинаю понимать, как 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не испытываю слабого чувства страха, когда вижу его в сигнатуре типа.

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

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-Type:

Давайте начнем с того, что 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]'
    ...

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

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

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

Таким образом, с помощью Existential-Quantification, foralls в dataопределениях означает, что содержащееся значение может иметь любой подходящий тип, а не то, что оно должно быть всех подходящих типов.

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

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

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

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

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

• В частности, в Haskell 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!

Приложение: Жаргон «выше», «ниже», «слева от». Они не имеют ничего общего с текстовыми способами написания типов и не имеют ничего общего с деревьями абстрактного синтаксиса. В абстрактном синтаксисе a 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

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

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

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

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

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

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

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

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

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

length :: [a] -> Int

Вот и все.

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

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

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

А как насчет простой логики первого порядка? 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 расширяется настолько далеко, насколько это возможно, вплоть до заключенных в скобки, и точно так же, как переменные, связанные в обычной лямбде, переменные типа, связанные с помощью a, 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 ...

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

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

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, если Хаскела поддерживает эту запись. Значение этого типа можно рассматривать как пару (или «продукт»), состоящую из типа 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, как если бы Хаскелл поддерживал эту запись.

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который, безусловно, должен как-то генерировать a. Более того, он должен иметь возможность генерировать значение типа aнезависимо от того, какой тип 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.

Кто-нибудь может полностью объяснить ключевое слово 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уровне термина для конкретной реализации.

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

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

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

С Existential-Quantification, foralls в dataопределениях означает, что содержащееся значение может быть любого подходящего типа, а не того, что оно должно быть всех подходящих типов. - ответ Ячиру

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

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

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 может быть применена функция к функции. Однако тип параметра можно выбрать только один раз в определении функции.

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

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

MkT :: forall a. a -> T

вид MkT :: a -> *

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

valueT :: forall a. [a]

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

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

[] :: [t]

Различия

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

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