Как выглядит нетривиальный комоноид?

Как упомянул Филип Дж. Ф., о комоноидах интересно поговорить в субструктурной логике. Поговорим о линейном лямбда-исчислении. Это очень похоже на обычное типизированное лямбда-исчисление, за исключением того, что каждая переменная должна использоваться ровно один раз.

Чтобы почувствовать, давайте посчитаем линейные функции заданных типов, т. Е.

a -> a

имеет ровно одного жителя, id. Пока

(a,a) -> (a,a)

имеет два, id и flip. Обратите внимание, что в обычном лямбда-исчислении (a,a) -> (a,a) имеет четыре жителя.

(a, b) ↦ (a, a)
(a, b) ↦ (b, b)
(a, b) ↦ (a, b)
(a, b) ↦ (b, a)

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

Вкратце, в чем смысл линейного ЖК? Что ж, мы можем использовать его для моделирования линейных эффектов или использования ресурсов. Если, например, у нас есть тип файла и несколько преобразователей, это может выглядеть так:

data File
open  :: String -> File
close :: File   -> ()      -- consumes a file, but we're ignoring purity right now
t1    :: File -> File
t2    :: File -> File

а затем допустимы следующие конвейеры:

close . t1 . t2 . open
close . t2 . t1 . open
close . t1      . open
close . t2      . open

но это "разветвленное" вычисление не

let f1 = open "foo"
    f2 = t1 f1
    f3 = t2 f1
in close f3

поскольку мы использовали f1 дважды.

Теперь вам может быть интересно узнать, какие вещи должны подчиняться линейным правилам. Например, я решил, что некоторые конвейеры не обязательно должны включать одновременно t1 и t2 (сравните предыдущее упражнение по перечислению). Кроме того, я представил функции open и close, которые успешно создают и уничтожают тип File, несмотря на то, что это нарушение линейности.

В самом деле, мы могли бы постулировать существование функций, которые нарушают линейность, но не все клиенты могут. Это очень похоже на монаду IO - все секреты находятся внутри реализации IO, так что пользователи работают в «чистом» мире.

И здесь на помощь приходит Comonoid.

class Comonoid m where
  destroy :: m -> ()
  split   :: m -> (m, m)

Тип, который создает экземпляр Comonoid в линейном лямбда-исчислении, является типом, который имеет правила уничтожения и дублирования с переносом. Другими словами, это тип, который вообще не очень привязан к линейному лямбда-исчислению.

Поскольку Haskell вообще не реализует правила линейного лямбда-исчисления, мы всегда можем создать экземпляр Comonoid

instance Comonoid a where
  destroy a = ()
  split a   = (a, a)

Или, возможно, другой способ думать об этом заключается в том, что Haskell - это линейная система LC, которая просто создает экземпляры Comonoid для каждого типа и автоматически применяет destroy и split для вас.

1. Моноид в обычном смысле - это то же самое, что категорический моноид в категории множеств. Можно было бы ожидать, что комоноид в обычном смысле - это то же самое, что категорический комоноид в категории множеств. Но каждое множество в категории множеств является комоноидом тривиальным образом, поэтому, по-видимому, нет некатегориального описания комоноидов, которое было бы параллельно описанию моноидов.
2. Точно так же, как монада - это моноид в категории эндофункторов (в чем проблема?), Комонада - это комоноид в категории эндофункторов (в чем проблема?) Так что да, любая комонада в Haskell была бы примером комоноида.

Что ж, один из способов, которым мы можем думать о моноиде, - это привязка к любой конкретной конструкции продукта, которую мы используем, поэтому в Set мы возьмем эту сигнатуру:

mul : A * A -> A
one : A

к этому:

dup : A -> A * A
one : A

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

div : A -> A + A
one : A

где + - помеченная сумма. Здесь мы, по сути, имеем, что каждый отдельный термин, который находится в этом типе, всегда готов произвести новый бит, который неявно выводится из тега, используемого для обозначения левого или правого экземпляра A. Лично я думаю, это чертовски круто. Я думаю, что классная версия того, о чем люди говорили выше, - это когда вы специально конструируете это не для моноидов, а для моноидных действий.

Говорят, что моноид M действует на множестве A, если существует функция

act : M * A -> A

где у нас есть следующие правила

act identity a = a
act f (act g a) = act (f * g) a

Если мы хотим сотрудничества, чего именно мы хотим?

act : A -> M * A

это порождает поток типа нашего комоноида! У меня много проблем с разработкой законов для этих систем, но я думаю, что они должны быть где-то поблизости, так что я собираюсь продолжить поиск сегодня вечером. Если кто-то может сказать мне им или что я ошибаюсь в этих вещах в той или иной степени, это тоже будет интересно.

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

В этом случае существует взаимное соответствие между моноидными и комоноидными объектами, поскольку вы можете просто взять сопряженное или транспонированное отображение продукта и единицы, чтобы получить копроизведение и счетчик, удовлетворяющие аксиомам комоноидов.

В некоторых разделах физики очень часто можно увидеть объекты, которые имеют как алгебру, так и структуру коалгебры с некоторыми аксиомами совместимости. Двумя наиболее распространенными случаями являются алгебры Хопфа и алгебры Фробениуса. Они очень удобны для построения запутанных или коррелированных состояний или решений.

В программировании простейшим нетривиальным примером, который я могу придумать, были бы указатели с подсчетом ссылок, такие как shared_ptr в C ++ и Rc в Rust, а также их слабые эквиваленты. Вы можете скопировать их, что является нетривиальной операцией, которая увеличивает счетчик ссылок (так что две копии отличаются от исходного состояния). Вы можете перетащить (вызвать деструктор) один, что нетривиально, потому что он снижает счетчик ссылок любого другого указателя с пересчетом, указывающего на тот же фрагмент данных.

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

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