Почему нет ключевого слова "Exist" в Haskell для экзистенциальной квантификации?

В соответствии с документацией GHC, с учетом следующего объявления:

data Foo = forall a. MkFoo a (a -> Bool)
           | Nil

то

MkFoo :: forall a. a -> (a -> Bool) -> Foo

Является (почти) изоморфным следующей декларации псевдо-Хаскелла

MkFoo :: (exists a . (a, a -> Bool)) -> Foo

Поэтому нет необходимости в отдельном ключе "Exist". Потому что:

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

Но я не уверен, что это значит. Может кто-нибудь объяснить мне, почему мы можем использовать универсальный квантификатор для выражения экзистенциальной квантификации?

Ответы

Ответ 1

В логике (классической или интуиционистской) формулы

(exists x. p x) -> q
forall x. (p x -> q)

эквивалентны (заметим, что q не зависит от x выше). Это можно использовать для выражения экзистенциальной квантификации в терминах универсальной квантификации, если экзистенциальное лежит в левой части на импликации. (Здесь классический доказательство.)

В функциональном программировании вы можете добиться того же. Вместо написания

-- Pseudo-Haskell follows
f :: (exists a. (a, a->Int)) -> Int
f (x,h) = h x

мы можем использовать

-- Actual Haskell
f :: forall a. (a, a->Int) -> Int
f (x,h) = h x

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

Экзистенциальная квантификация по-прежнему необходима, когда она встречается не слева от стрелки. Например,

g :: exists a. (a, a->Int)
g = (2 :: Int, \x -> x+3)

Увы, Haskell решил не включать эти типы. Вероятно, этот выбор был сделан для того, чтобы удержать уже сложную систему типов от слишком сложного.

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

data Ex where
  E :: forall a. (a, a->Int) -> Ex
g :: Ex
g = E (2 :: Int, \x -> x+3)

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

g :: forall r. (forall a. (a, a->Int) -> r) -> r
g k = k (2 :: Int, \x -> x+3)

Ответ 2

Первое, что нужно заметить, это то, что квант forall отображается в правой части знака равенства, поэтому он связан с конструктором данных (не типа): MkFoo, Таким образом, тип Foo ничего не говорит о a.

Мы снова сталкиваемся с a, когда пытаемся сопоставить шаблон по значениям типа Foo. В этот момент вы почти ничего не узнаете о компонентах MkFoo, за исключением того, что они существуют (должен существовать тип, используемый для вызова MkFoo), и что первый компонент может быть использован как аргумент второму компоненту, который является функцией:

f :: Foo -> Bool
f (MkFoo val fn) = fn val

Ответ 3

Если вы посмотрите на тип конструкторов данных, вы заметите, что мы аналогичным образом используем ->, чтобы как-то означать продукт. Например.

(:) :: a -> [a] -> [a]

действительно означает, что мы используем (:) для упаковки a вместе со списком типа [a] и доставляем список типа [a].

В вашем примере использование forall просто означает, что MkFoo, как конструктор, хочет упаковать любой тип a. Когда вы читаете (exists a . (a, a -> Bool)) -> Foo в документации GHC, вы должны думать об этом как о неопознанной версии исходного типа MkFoo. Соответствующая непереработанная версия (:) будет (a, [a]) -> [a].