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

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

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

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

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

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

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

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

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

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

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, мы сможем подтвердить, что State — это именно наша классическая монада состояния. Обратите внимание, что мы можем взять противоположную композицию и получить Costate Comonad (она же магазинная комонада).

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

этот материал по-другому освещен в статье Дерека Элкинса в The Monad Reader 13 -- Расчет монад с помощью теории категорий: http://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

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

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

Две ссылки.

1) Category-extras доставляет, как всегда, представление о присоединениях и о том, как из них возникают монады. Как обычно, хорошо подумать, но довольно мало документации: 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

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

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

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

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

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

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

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

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

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

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

Итак, в данном случае категория Т-алгебр — это как раз категория моноидных структур, определимых в 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 в подходящем смысле.

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

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

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

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

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

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

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

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

С другой стороны, как мы уже отмечали, между монадами и дополнениями к (T-)алгебрам также существует соответствие 1-1. Сопряжения, в терминах Маклейна, — это «способ выражения эквивалентности категорий». В типичной настройке дополнений <F,G>:X->A, где F является своего рода «генератором свободной алгебры», а G — «забывающим функтором», соответствующая монада будет (посредством использования Т-алгебр) описывать, как (и когда) алгебраическая структура 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 не более чем синтаксическим сахаром (что, конечно, очень важно на практике).