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

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

Типы сигм

Точно так же, как Π-типы (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))

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

{-# 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

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

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