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

Question

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

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

552 5

haskell monads functor category-theory

5 ответов:

Comments

Ничего не найдено.

sclv · Accepted Answer · 2014-03-26 07:33:19

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

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

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

примыкание между f (D - > C) и g (C -> D), записанные f -| g, могут быть охарактеризованы несколькими способами. Мы будем использовать описание countit / 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 из определения countit / 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 / countit следующим образом:
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, мы можем подтвердить, что состояние-это именно наша классическая монада состояния. Обратите внимание, что мы можем занять противоположную состав и получить ребристый Comonad (ака comonad магазине).

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

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

кроме того, последние расширения Kan Hinze для оптимизации программной бумаги проходят через построение монады списка из примыкания между 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

copumpkin · Accepted Answer · 2012-05-09 20:41:28

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

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

takosuke · Accepted Answer · 2012-02-14 11:19:26

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

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

пусть 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-алгебра.

In сюда (h = foldr ( * ) a0, функция, которая "заменяет"(:) С (*)и карты [] до a0, личность).

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

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

он также характеризует списки как универсальные объекты в 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) чтобы проверить ваше понимание.

Bartosz Milewski · Accepted Answer · 2012-02-14 11:56:11

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

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

Я должен сказать, я не знаю.

tokosuke · Accepted Answer · 2012-02-14 11:56:02

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

прежде всего, существует для данной монады 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 какая-то бесплатно генератор алгебре и Г 'забывчивый функтор',в соответствующая монада будет (с помощью T-алгебр) описывать, как (и когда) алгебраическая структура A строится на объектах X.

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

по-видимому, этот вид приложений является одним из основных мотивов создателей категории Теория (Маклейн, Эйленберг и др.), а именно, установить естественную эквивалентность категорий и перенести известный метод в одну категорию к другому (например, гомологические методы к топологическим пространствам, алгебраические методы к программированию и т. д.). Здесь примыкающие и монады являются незаменимыми инструментами для использования этой связи категорий. (Кстати, понятие монад (и его двойственных, комонад) настолько общее, что можно даже зайти так далеко, чтобы определить "когомологии" Типы Хаскелл.Но у меня нет я еще об этом подумал.)

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

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

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