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

Ответ 1

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

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

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)

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

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

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.

Ответ 2

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

Ответ 3

Ну, один способ, которым мы можем думать о моноиде, привязан к любой конкретной конструкции продукта, которую мы используем, поэтому в 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

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