Как выразить типы экзистенции с использованием полиморфизма типа более высокого ранга (ранга-N)?

Ответ 1

Оказывается, что экзистенциальные типы являются лишь частным случаем Σ-типов (сигма-типы). Что они?

Типы сигм

Подобно тому, как Π-типы (типы pi) обобщают наши обычные типы функций, позволяя полученному типу зависеть от значения его аргумента, Σ-типы обобщают пары, позволяя типу второго компонента зависеть от значения первый.

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

data Sigma (a :: *) (b :: a -> *)
    = SigmaIntro
        { fst :: a
        , snd :: b fst
        }

-- special case is a non-dependent pair
type Pair a b = Sigma a (\_ -> b)

Предполагая * :: * (т.е. несогласованный Set : Set), мы можем определить exists a. a как:

Sigma * (\a -> a)

Первый компонент является типом, а второй - значением этого типа. Некоторые примеры:

foo, bar :: Sigma * (\a -> a)
foo = SigmaIntro Int  4
bar = SigmaIntro Char 'a'

exists a. a бесполезен - мы не знаем, какой тип внутри, поэтому единственными операциями, которые могут с ним работать, являются агностические функции типа id или const. Допустим его до exists a. F a или даже exists a. Show a => F a. Учитывая F :: * -> *, первый случай:

Sigma * F   -- or Sigma * (\a -> F a)

Второй немного сложнее. Мы не можем просто взять экземпляр класса типа Show a и поместить его где-то внутри. Однако, если нам предоставляется словарь Show a (типа ShowDictionary a), мы можем упаковать его с фактическим значением:

Sigma * (\a -> (ShowDictionary a, F a))
-- inside is a pair of "F a" and "Show a" dictionary

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

Отступление: благодаря типам ограничений, можно присвоить класс типа конкретному типу данных. Во-первых, нам нужны некоторые языковые прагмы и один импорт:

{-# LANGUAGE ConstraintKinds, GADTs, KindSignatures  #-}
import GHC.Exts -- for Constraint

GADT уже дают нам возможность упаковать класс типа вместе с конструктором, например:

data BST a where
    Nil  :: BST a
    Node :: Ord a => a -> BST a -> BST a -> BST a

Однако мы можем сделать еще один шаг:

data Dict :: Constraint -> * where
    D :: ctx => Dict ctx

Он работает так же, как пример BST выше: сопоставление шаблонов на D :: Dict ctx дает нам доступ ко всему контексту ctx:

show' :: Dict (Show a) -> a -> String
show' D = show

(.+) :: Dict (Num a) -> a -> a -> a
(.+) D = (+)

Мы также получаем вполне естественное обобщение для экзистенциальных типов, которые определяют количество более переменных типа, таких как exists a b. F a b.

Sigma * (\a -> Sigma * (\b -> F a b))
-- or we could use Sigma just once
Sigma (*, *) (\(a, b) -> F a b)
-- though this looks a bit strange

Кодировка

Теперь возникает вопрос: можем ли мы кодировать Σ-типы только с Π-типами? Если да, то кодировка экзистенциального типа - это особый случай. Во всей славе я представляю вам фактическую кодировку:

newtype SigmaEncoded (a :: *) (b :: a -> *)
    = SigmaEncoded (forall r. ((x :: a) -> b x -> r) -> r)

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

(∃x)R(x) ⇔ ¬(∀x)¬R(x) ⇔ (∀x)(R(x) → ⊥) → ⊥

forall r. r почти ⊥, поэтому с небольшим количеством перезаписи мы получаем:

(∀x)(R(x) → r) → r

И, наконец, представляя универсальное квантификацию как зависимую функцию:

forall r. ((x :: a) -> R x -> r) -> r

Кроме того, давайте взглянем на тип кодов, закодированных Церковью. Мы получаем очень похожий вид:

Pair a b  ~  forall r. (a -> b -> r) -> r

Нам просто нужно выразить тот факт, что b может зависеть от значения a, что мы можем сделать, используя зависимую функцию. И снова мы получаем тот же тип.

Соответствующие функции кодирования/декодирования:

encode :: Sigma a b -> SigmaEncoded a b
encode (SigmaIntro a b) = SigmaEncoded (\f -> f a b)

decode :: SigmaEncoded a b -> Sigma a b
decode (SigmaEncoded f) = f SigmaIntro
-- recall that SigmaIntro is a constructor

Частный случай на самом деле упрощает вещи, достаточные для того, чтобы он был выражен в Haskell, давайте взглянем:

newtype ExistsEncoded (F :: * -> *)
    = ExistsEncoded (forall r. ((x :: *) -> (ShowDictionary x, F x) -> r) -> r)
    -- simplify a bit
    = ExistsEncoded (forall r. (forall x. (ShowDictionary x, F x) -> r) -> r)
    -- curry (ShowDictionary x, F x) -> r
    = ExistsEncoded (forall r. (forall x. ShowDictionary x -> F x -> r) -> r)
    -- and use the actual type class
    = ExistsEncoded (forall r. (forall x. Show x => F x -> r) -> r)

Обратите внимание, что мы можем просмотреть f :: (x :: *) -> x -> x как f :: forall x. x -> x. То есть функция с дополнительным аргументом * ведет себя как полиморфная функция.

И некоторые примеры:

showEx :: ExistsEncoded [] -> String
showEx (ExistsEncoded f) = f show

someList :: ExistsEncoded []
someList = ExistsEncoded $ \f -> f [1]

showEx someList == "[1]"

Обратите внимание, что someList фактически построено через encode, но мы отбросили аргумент a. Это потому, что Haskell выведет, что x в части forall x., которую вы на самом деле имеете в виду.

От Π до Σ?

Как ни странно (хотя и вне сферы действия этого вопроса), вы можете кодировать Π-типы через Σ-типы и обычные типы функций:

newtype PiEncoded (a :: *) (b :: a -> *)
    = PiEncoded (forall r. Sigma a (\x -> b x -> r) -> r)
-- \x -> is lambda introduction, b x -> r is a function type
-- a bit confusing, I know

encode :: ((x :: a) -> b x) -> PiEncoded a b
encode f = PiEncoded $ \sigma -> case sigma of
    SigmaIntro a bToR -> bToR (f a)

decode :: PiEncoded a b -> (x :: a) -> b x
decode (PiEncoded f) x = f (SigmaIntro x (\b -> b))

Ответ 2

Я нашел anwer в Доказательства и типы Жан-Ив Жирар, Ив Лафонт и Пол Тейлор.

Представьте, что у нас есть тип одного аргумента t :: * -> * и построим экзистенциальный тип, который содержит t a для некоторого a: exists a. t a. Что мы можем сделать с таким типом? Чтобы вычислить что-то из этого, нам нужна функция, которая может принимать t a для произвольного a, что означает функцию типа forall a. t a -> b. Зная это, мы можем кодировать экзистенциальный тип просто как функцию, которая принимает функции типа forall a. t a -> b, передает им экзистенциальное значение и возвращает результат b:

{-# LANGUAGE RankNTypes #-}

newtype Exists t = Exists (forall b. (forall a. t a -> b) -> b)

Создание экзистенциального значения теперь легко:

exists :: t a -> Exists t
exists x = Exists (\f -> f x)

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

unexists :: (forall a. t a -> b) -> Exists t -> b
unexists f (Exists e) = e f

Однако чисто экзистенциальные типы очень мало используются. Мы не можем делать ничего разумного с той ценностью, о которой мы ничего не знаем. Чаще всего нам нужен экзистенциальный тип с ограничением типа. Процедура такая же, просто добавим ограничение типа класса для a. Например:

newtype ExistsShow t = ExistsShow (forall b. (forall a. Show a => t a -> b) -> b)

existsShow :: Show a => t a -> ExistsShow t
existsShow x = ExistsShow (\f -> f x)

unexistsShow :: (forall a. Show a => t a -> b) -> ExistsShow t -> b
unexistsShow f (ExistsShow e) = e f

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