Зачем нам нужны контейнеры?

Question

(Как оправдание: заголовок имитирует заголовок " Зачем нам нужны монады?")

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

⟦_⟧ᶜ : ∀ {α β γ} -> Container α β -> Set γ -> Set (α ⊔ β ⊔ γ)
⟦ Sh ◃ Pos ⟧ᶜ A = ∃ λ sh -> Pos sh -> A

Kᶜ : ∀ {α β} -> Set α -> Container α β
Kᶜ A = A ◃ const (Lift ⊥)

мы в основном используем Σ а не формы и позиции.

Тип строго положительных свободных монад над контейнерами имеет довольно простое определение, но тип Freer монады выглядят проще для меня (и в некотором смысле Freer монады даже лучше чем обычно Free монады, как описано в статье).

Так, что мы можем сделать с контейнерами более хорошим способом, чем с описаниями или чем-то еще?

Answer 1

На мой взгляд, ценность контейнеров (как в теории контейнеров) заключается в их однородности. Это единообразие дает значительные возможности для использования контейнерных представлений в качестве основы для исполняемых спецификаций и, возможно, даже для машинного вывода программ.

Контейнеры: теоретический инструмент, а не хорошая стратегия представления данных во время выполнения

Я бы не рекомендовал фиксированные точки (нормализованных) контейнеров как хороший универсальный способ реализации рекурсивных структур данных. То есть полезно знать, что данный функтор имеет (до iso) представление в виде контейнера, потому что он сообщает вам, что можно реализовать универсальную функциональность контейнера (которая легко реализуется раз и навсегда благодаря единообразию) к вашему конкретному функтору, и какое поведение вы должны ожидать. Но это не значит, что реализация контейнера будет эффективной любым практическим способом. Действительно, я обычно предпочитаю кодировки первого порядка (тэги и кортежи, а не функции) данных первого порядка.

Чтобы исправить терминологию, скажем, что тип Cont контейнеров (на Set, но доступны и другие категории) предоставляется конструктором <| упаковка двух полей, форм и позиций

S : Set
P : S -> Set

(Это та же сигнатура данных, которая используется для определения типа Sigma, или типа Pi, или типа W, но это не означает, что контейнеры совпадают с любой из этих вещей, или что эти вещи одинаковы как друг друга.)

Интерпретация такой вещи как функтор дается

[_]C : Cont -> Set -> Set
[ S <| P ]C X = Sg S \ s -> P s -> X  -- I'd prefer (s : S) * (P s -> X)
mapC : (C : Cont){X Y : Set} -> (X -> Y) -> [ C ]C X -> [ C ]C Y
mapC (S <| P) f (s , k) = (s , f o k)  -- o is composition

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

Описания денормализованных контейнеров

Никто не пытается утверждать, что в оперативном Nat <| Fin дает эффективную реализацию списков, просто благодаря этой идентификации мы узнаем что-то полезное о структуре списков.

Позвольте мне сказать кое-что об описаниях. Для ленивых читателей, позвольте мне восстановить их.

data Desc : Set1 where
  var : Desc
  sg pi  : (A : Set)(D : A -> Desc) -> Desc
  one : Desc                    -- could be Pi with A = Zero
  _*_ : Desc -> Desc -> Desc    -- could be Pi with A = Bool

con : Set -> Desc   -- constant descriptions as singleton tuples
con A = sg A \ _ -> one

_+_ : Desc -> Desc -> Desc   -- disjoint sums by pairing with a tag
S + T = sg Two \ { true -> S ; false -> T }

Значения в Desc опишите функторы, чьи фиксированные точки дают типы данных. Какие функторы они описывают?

[_]D : Desc -> Set -> Set
[ var    ]D X = X
[ sg A D ]D X = Sg A \ a -> [ D a ]D X
[ pi A D ]D X = (a : A) -> [ D a ]D X
[ one    ]D X = One
[ D * D' ]D X = Sg ([ D ]D X) \ _ -> [ D' ]D X

mapD : (D : Desc){X Y : Set} -> (X -> Y) -> [ D ]D X -> [ D ]D Y
mapD var      f x        = f x
mapD (sg A D) f (a , d)  = (a , mapD (D a) f d)
mapD (pi A D) f g        = \ a -> mapD (D a) f (g a)
mapD one      f <>       = <>
mapD (D * D') f (d , d') = (mapD D f d , mapD D' f d')

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

Обратите внимание, что у каждого контейнера есть описание:

sg S \ s -> pi (P s) \ _ -> var

Но также верно, что каждое описание имеет представление в виде изоморфного контейнера.

ShD  : Desc -> Set
ShD D = [ D ]D One

PosD : (D : Desc) -> ShD D -> Set
PosD var      <>       = One
PosD (sg A D) (a , d)  = PosD (D a) d
PosD (pi A D) f        = Sg A \ a -> PosD (D a) (f a)
PosD one      <>       = Zero
PosD (D * D') (d , d') = PosD D d + PosD D' d'

ContD : Desc -> Cont
ContD D = ShD D <| PosD D

То есть контейнеры - это нормальная форма для описаний. Это упражнение, чтобы показать, что [ D ]D X естественно изоморфно [ ContD D ]C X, Это облегчает жизнь, потому что, чтобы сказать, что делать с описаниями, в принципе достаточно сказать, что делать с их обычными формами, контейнерами. Выше mapD Операция, в принципе, может быть получена путем объединения изоморфизмов с единообразным определением mapC,

Дифференциальная структура: контейнеры показывают путь

Точно так же, если у нас есть понятие равенства, мы можем сказать, что контексты с одним отверстием для контейнеров равномерно

_-[_] : (X : Set) -> X -> Set
X -[ x ] = Sg X \ x' -> (x == x') -> Zero

dC : Cont -> Cont
dC (S <| P) = (Sg S P) <| (\ { (s , p) -> P s -[ p ] })

То есть форма контекста с одним отверстием в контейнере представляет собой пару формы исходного контейнера и положения отверстия; позиции являются исходными позициями, кроме позиции отверстия. Это проверенная версия "умножить на индекс, уменьшить индекс" при дифференциации степенных рядов.

Этот унифицированный подход дает нам спецификацию, из которой мы можем вывести многовековую программу для вычисления производной многочлена.

dD : Desc -> Desc
dD var = one
dD (sg A D) = sg A \ a -> dD (D a)
dD (pi A D) = sg A \ a -> (pi (A -[ a ]) \ { (a' , _) -> D a' }) * dD (D a)
dD one      = con Zero
dD (D * D') = (dD D * D') + (D * dD D')

Как я могу проверить правильность моего производного оператора для описаний? Сверяя его с производными контейнеров!

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

На "Фрире" монады

Одна последняя вещь. Freer хитрость сводится к перестановке произвольного функтора определенным образом (переключение на Haskell)

data Obfuncscate f x where
  (:<) :: forall p. f p -> (p -> x) -> Obfuncscate f x

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

data Obfuncscate f x where
  (:<) :: pi (s :: exists p. f p) -> (fst s -> x) -> Obfuncscate f x

чтобы (exists p. f p) представляет фигуры (где вы можете выбрать свое представление позиций, затем отметить каждое место с его позицией), и fst выбирает экзистенциального свидетеля из фигуры (представление позиции, которое вы выбрали). Заслуга в том , что он явно строго положительный , потому что это контейнерная презентация.

В Хаскеле, конечно, вам нужно вычеркнуть экзистенциальное, которое, к счастью, оставляет зависимость только от проекции типа. Это слабость экзистенциального, которая оправдывает эквивалентность Obfuncscate f а также f, Если вы попробуете тот же трюк в теории зависимых типов с сильными экзистенциалами, кодировка утратит свою уникальность, потому что вы можете проецировать и различать различные варианты представления позиций. То есть я могу представлять Just 3 от

Just () :< const 3

или

Just True :< \ b -> if b then 3 else 5

и в Coq, скажем, они явно различимы.

Задача: охарактеризовать полиморфные функции

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

Если у вас есть некоторые

f : {X : Set} -> [ S <| T ]C X -> [ S' <| T' ]C X

он (расширенно) определяется следующими данными, в которых вообще не упоминаются элементы:

toS    : S -> S'
fromP  : (s : S) -> P' (toS s) -> P s

f (s , k) = (toS s , k o fromP s)

То есть единственный способ определить полиморфную функцию между контейнерами - это сказать, как преобразовать входные фигуры в выходные, а затем сказать, как заполнить выходные позиции из входных позиций.

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

Задача: захватить "транспонируемость"

Учитывая два функтора, f а также g Легко сказать, каков их состав f o g является: (f o g) x оборачивает вещи в f (g x), давая нам " f -структуры g -структуры ". Но вы можете легко навязать дополнительное условие, что все g структуры хранятся в f структура имеет одинаковую форму?

Скажем так f >< g захватывает перемещаемый фрагмент f o g где все g формы одинаковы, так что мы можем также превратить вещь в g -структура f -структурах. Например, пока [] o [] дает рваные списки списков, [] >< [] дает прямоугольные матрицы; [] >< Maybe дает списки, которые либо все Nothing или все Just,

Дать >< для вашего предпочтительного представления строго положительных функторов. Для контейнеров это так просто.

(S <| P) >< (S' <| P') = (S * S') <| \ { (s , s') -> P s * P' s' }

Заключение

Контейнеры в их нормализованной форме Sigma-then-Pi не предназначены для эффективного машинного представления данных. Но знание того, что данный функтор, реализованный, однако, имеет представление в виде контейнера, помогает нам понять его структуру и предоставить ему полезное оборудование. Многие полезные конструкции могут быть даны абстрактно для контейнеров, раз и навсегда, когда они должны быть приведены в каждом конкретном случае для других презентаций. So, yes, it is a good idea to learn about containers, if only to grasp the rationale behind the more specific constructions you actually implement.