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

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

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

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

Нет. (Что ж, может быть, Дон Стюарт сможет.)

Вот препятствия на пути к простому, ясному объяснению или для всего :

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

• Это квантор типа . Если вы не видели System F и немного попрактиковались в написании полиморфных типов, вы найдете для всех запутанным. Опыт работы с 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 для ввода а . Например, я могу передать функцию (+ 1) или функцию reverse . Вы можете думать о forall как о том, что «я должен выбрать тип сейчас». (Техническое слово для выбора типа - создание экземпляра .)

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

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

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

Примеры:

• В forall a. [a] -> [a] , forall выше стрелки; то, что слева от стрелки - [a] .

• В

   во всем мире. (forall e x. n e x -> f -> Fact x f)
   -> Блок n e x -> f -> Факт x f
  

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

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

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

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

Итак, рассмотрим функцию 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 ab , уже предполагает «применить функцию 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 на ясном, простом английском языке

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

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

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

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

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

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

length :: [a] -> Int

Вот и все.

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

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