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

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

Последнее. Тройка 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 выберет экзистенциального свидетеля из формы (выбранное положение). Это имеет смысл быть явно строго положительным, потому что это представление контейнера.

В Haskell, конечно же, вы должны выработать экзистенциальный, который, к счастью, оставляет зависимость только от проекции типа. Это слабость экзистенциального, которая оправдывает эквивалентность 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 не предназначены для эффективного машинного представления данных. Но знание того, что данный функтор, выполненный, однако, имеет представление в виде контейнера, помогает нам понять его структуру и предоставить ему полезное оборудование. Многие полезные конструкции могут быть переданы абстрактно для контейнеров один раз для всех, когда они должны передаваться в каждом случае для других презентаций. Итак, да, это хорошая идея, чтобы узнать о контейнерах, только чтобы понять обоснование более конкретных конструкций, которые вы на самом деле реализуете.