Монады как дополнения

Question

Я читал про монады в теории категорий. Одно определение монад использует пару сопряженных функторов. Монада определяется циклом с использованием этих функторов. Очевидно, что присоединения очень важны в теории категорий, но я не видел никакого объяснения монад Хаскелла в терминах присоединенных функторов. Кто-нибудь задумывался над этим?

Answer 1

Редактировать : Просто ради удовольствия, я собираюсь сделать это правильно.Оригинальный ответ сохранен ниже

Текущий код присоединения для дополнительных категорий теперь находится в пакете дополнений: http://hackage.haskell.org/package/adjunctions

Я просто собираюсь проработать монаду состояния явно и просто.Этот код использует Data.Functor.Compose из пакета преобразователей, но в остальном он самодостаточен.

Соединение между f (D -> C) и g (C -> D), написанное f - |г, можно охарактеризовать несколькими способами.Мы будем использовать описание count / unit (epsilon / eta), которое дает два естественных преобразования (морфизмы между функторами).

class (Functor f, Functor g) => Adjoint f g where
     counit :: f (g a) -> a
     unit   :: a -> g (f a)

Обратите внимание, что число «a» на самом деле является функтором тождественности в C, а число «a» на самом деле является функтором тождественности в D.

Мы также можем восстановитьопределение присоединения hom-set из определения количества / единицы.

phiLeft :: Adjoint f g => (f a -> b) -> (a -> g b)
phiLeft f = fmap f . unit

phiRight :: Adjoint f g => (a -> g b) -> (f a -> b)
phiRight f = counit . fmap f

В любом случае, теперь мы можем определить монаду из присоединения единицы / единицы следующим образом:

instance Adjoint f g => Monad (Compose g f) where
    return x = Compose $ unit x
    x >>= f  = Compose . fmap counit . getCompose $ fmap (getCompose . f) x

Теперь мы можем реализовать классическое соединение между (a,) и (a ->):

instance Adjoint ((,) a) ((->) a) where
    -- counit :: (a,a -> b) -> b
    counit (x, f) = f x
    -- unit :: b -> (a -> (a,b))
    unit x = \y -> (y, x)

А теперь синоним типа

type State s = Compose ((->) s) ((,) s)

И если мы загрузим это в ghciМы можем подтвердить, что Государство является именно нашей классической государственной монадой.Обратите внимание, что мы можем взять противоположную композицию и получить Costate Comonad (также называемый Comonad магазина).

Существует множество других приставок, которые мы можем сделать в монады таким способом (например, (Bool,) Pair)Но они вроде странные монады.К сожалению, мы не можем делать дополнения, которые побуждают Reader и Writer непосредственно в Haskell приятным способом.Мы можем сделать Cont, но, как описывает copumpkin, для этого требуется присоединение из противоположной категории, поэтому он фактически использует другую "форму" класса типов "Сопряженный", которая обращает некоторые стрелки.Эта форма также реализована в другом модуле пакета дополнений.

этот материал по-разному описан в статье Дерека Элкинса в «Монадном читателе» 13 - «Вычисление монад с помощью теории категорий»: http://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

Кроме того, в недавней статье Kin Extensions для оптимизации программ, проведенной Хинце, рассказывается о построении монады списка из соединения между Mon и Set: http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf

---

Старый ответ:

Две ссылки.

1) Экстра-категории, как всегда, предоставляют представление дополнений и то, как из них возникают монады.Как обычно, хорошо подумать, но довольно легко документировать: http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor-Adjunction.html

2) -Кафе также проводит многообещающее, но краткое обсуждение роли присоединения.Некоторые из которых могут помочь в интерпретации дополнительных категорий: http://www.haskell.org/pipermail/haskell-cafe/2007-December/036328.html

Answer 2

Дерек Элкинс недавно демонстрировал мне за обедом, как Cont Monad возникает из-за того, что он создает (_ -> k) контравариантный функтор с самим собой, поскольку он самосопряженный.Вот как вы получаете (a -> k) -> k из этого.Однако его количество приводит к исключению двойного отрицания, которое не может быть написано на Хаскеле.

Для некоторого кода Agda, который иллюстрирует и доказывает это, см. http://hpaste.org/68257.

Answer 3

Это старая ветка, но я нашел вопрос интересным, поэтому я сделал некоторые вычисления сам. Надеюсь, Бартош все еще там и мог бы прочитать это ..

На самом деле конструкция Эйленберга-Мура дает очень четкую картину в этом случае. (Я буду использовать нотацию CWM с синтаксисом, похожим на Haskell)

Пусть T будет монадой списка < T,eta,mu > (eta = return и mu = concat) и рассмотрим T-алгебру h:T a -> a.

(Обратите внимание, что T a = [a] - это свободный моноид <[a],[],(++)>, т. Е. Тождество [] и умножение (++).)

По определению h должен удовлетворять h.T h == h.mu a и h.eta a== id.

Теперь, некоторая простая погоня за диаграммой доказывает, что h фактически вызывает моноидную структуру на (определенную x*y = h[x,y]), и что h становится моноидным гомоморфизмом для этой структуры.

И наоборот, любая моноидная структура < a,a0,* >, определенная в Haskell, естественно определяется как T-алгебра.

Таким образом (h = foldr ( * ) a0, функция, которая «заменяет» (:) на (*) и отображает [] в a0, тождество).

Итак, в данном случае категория T-алгебр - это просто категория моноидных структур, определяемых в Haskell, HaskMon.

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

Он также характеризует списки как универсальные объекты в HaskMon, точно так же, как бесплатные продукты в Grp, полиномиальные кольца в CRng и т. Д.

Присоединение, соответствующее вышеуказанной конструкции: < F,G,eta,epsilon >

, где

• F:Hask -> HaskMon, который переводит тип a в 'свободный моноид, генерируемый a', то есть [a],
• G:HaskMon -> Hask, забывчивый функтор (забудьте умножение),
• eta:1 -> GF, естественная трансформация, определяемая \x::a -> [x],
• epsilon: FG -> 1, естественное преобразование, определенное функцией складывания выше («каноническая сюррекция» от свободного моноида к его частному моноиду)

Далее есть еще одна «категория Клейсли» и соответствующее присоединение. Вы можете проверить, что это просто категория типов Haskell с морфизмами a -> T b, где его композиции задаются так называемой «композицией Клейсли» (>=>). Типичный программист на Haskell найдет эту категорию более знакомой.

Наконец, как показано в CWM, категория T-алгебр (соответственно категория Клейсли) становится конечным (соответственно начальным) объектом в категории адъюнкций, которые определяют список монады Т в подходящем смысле.

Я предлагаю сделать аналогичные вычисления для функтора бинарного дерева T a = L a | B (T a) (T a), чтобы проверить ваше понимание.

Answer 4

Я нашел стандартные конструкции вспомогательных функторов для любой монады Эйленберга-Мура, но я не уверен, добавляет ли это какую-либо информацию о проблеме. Вторая категория в построении - это категория T-алгебр. Алгебра T добавляет «продукт» к начальной категории.

Так, как это будет работать для монады списка? Функтор в монаде списка состоит из конструктора типа, например Int->[Int], и отображения функций (например, стандартное применение map к спискам). Алгебра добавляет отображение из списков в элементы. Одним из примеров будет добавление (или умножение) всех элементов списка целых чисел. Функтор F принимает любой тип, например Int, и отображает его в алгебру, определенную в списках Int, где произведение определяется монадным соединением (или наоборот, соединение определяется как произведение). Забывчивый функтор G берет алгебру и забывает произведение. Пара F, G сопряженных функторов затем используется для построения монады обычным способом.

Я должен сказать, что я не мудрый.

Answer 5

Если вам интересно, вот некоторые мысли неэксперта о роли монад и приставок в языках программирования:

Прежде всего, существует для данной монады T уникальное присоединение к категории Клейсли T. В Haskell использование монад в основном сводится к операциям в этой категории. (которая по сути является категорией свободных алгебр, без факторов). Фактически, все, что можно сделать с монадой на Хаскеле, - это составить некоторые морфизмы Клейсли: введите a->T b с помощью выражений do, (>>=) и т. д., чтобы создать новый морфизм. В этом контексте роль монад ограничивается только экономикой нотации. Один из них использует ассоциативность морфизмов для записи (скажем) [0,1,2] вместо (Cons 0 (Cons 1 (Cons 2 Nil))), то есть вы можете написать последовательность как последовательность, не как дерево.

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

Это мой ответ на ваш оригинальный вопрос, но мне любопытно, что эксперты по Haskell говорят по этому поводу.

С другой стороны, как мы уже отмечали, существует также соответствие 1-1 между монадами и присоединения к (T-) алгебрам. Адъюнкты, с точки зрения Маклейна, - это «путь чтобы выразить эквивалентность категорий. В типичной установке примыканий <F,G>:X->A, где F - это своего рода 'генератора свободной алгебры' и G 'функтора забвения', соответствующей монаде (посредством использования T-алгебр) опишет, как (и когда) алгебраическая структура A строится на объектах X.

В случае Hask и монады T списка, структура, которую вводит T, такова, что моноида, и это может помочь нам установить свойства (в том числе правильность) кода с помощью алгебраического методы, которые обеспечивает теория моноидов. Например, функция foldr (*) e::[a]->a может легко увидеть как ассоциативную операцию, пока <a,(*),e> является моноидом, факт, который может быть использован компилятором для оптимизации вычислений (например, параллелизмом). Другое приложение состоит в том, чтобы идентифицировать и классифицировать «шаблоны рекурсии» в функциональном программировании, используя категориальные методы в надежде (частично) избавиться от «перехода к функциональному программированию», Y (произвольный рекурсивный комбинатор).

Видимо, такого рода приложения являются одной из основных мотиваций создателей теории категорий (Маклейн, Эйленберг и т. Д.), а именно, установить естественную эквивалентность категорий и перенести известный метод в одну категорию к другому (например, гомологические методы к топологическим пространствам, алгебраические методы к программированию и т. д.). Здесь примыкания и монады являются незаменимыми инструментами для использования этой связи категорий. (Между прочим, понятие монад (и их двойственных, комонад) является настолько общим, что можно даже пойти так далеко, чтобы определить «когомологии» Типы на Haskell. Но я еще не подумал.)

Что касается недетерминированных функций, о которых вы упоминали, я могу сказать гораздо меньше ... Но учтите это; если присоединение <F,G>:Hask->A для некоторой категории A определяет монаду списка T, должен быть уникальный «функтор сравнения» K:A->MonHask (категория моноидов, определяемая в Haskell), см. CWM. По сути, это означает, что ваша интересующая категория должна быть категорией моноидов в некоторой ограниченной форме (например, в ней могут отсутствовать некоторые частные, но не свободные алгебры) для определения монады списка.

Наконец, несколько замечаний:

Функтор бинарного дерева, о котором я упоминал в своей последней публикации, легко обобщается на произвольный тип данных T a1 .. an = T1 T11 .. T1m | .... А именно, любой тип данных в Haskell, естественно, определяет монаду (вместе с соответствующей категорией алгебр и категорией Клейсли), что является просто результатом того, что любой конструктор данных в Haskell является тотальным. Это еще одна причина, почему я считаю, что класс Monad в Haskell не намного больше, чем синтаксический сахар (что очень важно на практике, конечно).