Что делает ключевое слово `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-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

Чем это отличается от ранга-N-типов?

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

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

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

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

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

Answer 2

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

Резюме: A завершено объяснение ключевого слова 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 довольно четко относится к универсальному количественному определению , и в этом контексте термин экзистенциальный также имеет больше смысла, хотя было бы менее неловко, если бы было 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 5

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

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

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

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

Например, рассмотрим тип 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 6

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

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

Answer 7

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

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

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

                CONSTRAINTS LIBERATE, LIBERTIES CONSTRAIN

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

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

foo :: a -> a

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

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

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 должно принадлежать к наборучисел), освобождает термин «уровень» для нескольких возможных реализаций.

---

Теперь перейдем ко второму утверждению, которое действительно содержит объяснение 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 8

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

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

Объяснение того, почему forall в data определениях изоморфны (exists a. a) (псевдо-Haskell), можно найти в wikibooks "Haskell / Existentially quanified types" .

Ниже приводится краткая сводная информация:

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 на определение против функции приложение .

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

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

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

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

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

MkT :: forall a. a -> T

вид MkT :: a -> *

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

valueT :: forall a. [a]

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

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

[] :: [t]

Различия

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

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