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

Переменные типа с областью действия:

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

Непонятная точка: вы можете услышать, что, когда вы опускаете forall из типа, на самом деле он по-прежнему неявно присутствует. (от норманнского ответа: "Обычно эти языки опускают 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 in data означает, что значение, содержащее может иметь любой подходящий тип, а не то, что он должен иметь все подходящие типы.

Ответ 2

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

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

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

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

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

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

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

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

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

• runST должен сделать вашу голову болит. Типы высшего ранга (слева от стрелки) редко встречаются в дикой природе. Я рекомендую вам прочитать статью, в которой было представлено 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 требует математики и может быть понято только тем, кто изучал математику. Даже частичные объяснения трудно понять без математики. Но, возможно, мои частичные, не математические объяснения немного помогут. Иди почитай Launchbury и Peyton Jones на runST !

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

Примеры:

• В forall a. [a] → [a] 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
  

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

Ответ 3

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

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

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

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

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

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

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

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

length :: [a] -> Int

Это.

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

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

Ответ 4

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

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

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

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

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

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

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...

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

Ответ 5

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

Ключевое слово 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.

Ответ 6

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

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

Ответ 7

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

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

Ответ 8

Как существует экзистенциальный экзистенциальный?

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

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

Ниже приведен краткий стенографический отчет:

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 действительно означает" для всех ". Важным отличием является влияние forall на определение по сравнению с функцией .

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

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

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

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

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

MkT :: forall a. a -> T

вид MkT:: a -> *

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

valueT :: forall a. [a]

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

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

[] :: [t]

Различия

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

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