Монада - это просто моноид из категории эндофункторов, в чем проблема?

Во-первых, расширения и библиотеки, которые мы собираемся использовать:

{-# LANGUAGE RankNTypes, TypeOperators #-}

import Control.Monad (join)

Из них RankNTypes - единственный, который абсолютно необходим для нижеприведенного. Однажды я написал объяснение RankNTypes, которое некоторые люди, кажется, сочли полезным < / a>, поэтому я обращусь к этому.

Цитируя отличный ответ Тома Крокетта, мы имеем:

Монада - это ...

• Эндофунктор, T: X - ›X
• Естественное преобразование, μ: T × T - ›T, где × означает композицию функторов.
• Естественное преобразование, η: I - ›T, где I - это эндофунктор идентичности на X

... удовлетворяющие этим законам:

• μ(μ(T × T) × T)) = μ(T × μ(T × T))
• μ(η(T)) = T = μ(T(η))

Как нам перевести это в код Haskell? Что ж, давайте начнем с понятия естественного преобразования:

-- | A natural transformations between two 'Functor' instances.  Law:
--
-- > fmap f . eta g == eta g . fmap f
--
-- Neat fact: the type system actually guarantees this law.
--
newtype f :-> g =
    Natural { eta :: forall x. f x -> g x }

Тип формы f :-> g аналогичен типу функции, но вместо того, чтобы думать о нем как о функции между двумя типами (типа *), думайте о нем как о морфизм между двумя функторами (каждый вида * -> *). Примеры:

listToMaybe :: [] :-> Maybe
listToMaybe = Natural go
    where go [] = Nothing
          go (x:_) = Just x

maybeToList :: Maybe :-> []
maybeToList = Natural go
    where go Nothing = []
          go (Just x) = [x]

reverse' :: [] :-> []
reverse' = Natural reverse

По сути, в Haskell естественные преобразования - это функции из одного типа f x в другой тип g x, так что переменная типа x недоступна для вызывающего. Так, например, sort :: Ord a => [a] -> [a] нельзя превратить в естественное преобразование, потому что он разборчив в том, какие типы мы можем создать для a. Я часто думаю об этом интуитивно следующим образом:

• Функтор - это способ работы с содержимым чего-либо, не затрагивая структуру.
• Естественное преобразование - это способ работы с структурой чего-либо без касания и просмотра содержимого.

Теперь, разобравшись с этим, давайте займемся пунктами определения.

Первое предложение - это эндофунктор, T: X - ›X. Что ж, каждый Functor в Haskell является эндофунктором в том, что люди называют категорией Hask, чьи объекты являются типами Haskell (типа *) и чьи морфизмы являются функциями Haskell. Это звучит как сложное утверждение, но на самом деле это очень тривиально. Все это означает, что Functor f :: * -> * дает вам средства создания типа f a :: * для любого a :: * и функции fmap f :: f a -> f b из любого f :: a -> b, и что они подчиняются законам функторов.

Второе предложение: функтор Identity в Haskell (который поставляется с платформой, поэтому вы можете просто импортировать его) определяется следующим образом:

newtype Identity a = Identity { runIdentity :: a }

instance Functor Identity where
    fmap f (Identity a) = Identity (f a)

Таким образом, естественное преобразование η: I - ›T из определения Тома Крокетта может быть записано таким образом для любого Monad экземпляра t:

return' :: Monad t => Identity :-> t
return' = Natural (return . runIdentity)

Третье предложение: композиция двух функторов в Haskell может быть определена следующим образом (что также входит в состав платформы):

newtype Compose f g a = Compose { getCompose :: f (g a) }

-- | The composition of two 'Functor's is also a 'Functor'.
instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose fga) = Compose (fmap (fmap f) fga)

Итак, естественное преобразование μ: T × T - ›T из определения Тома Крокетта можно записать так:

join' :: Monad t => Compose t t :-> t
join' = Natural (join . getCompose)

Утверждение, что это моноид в категории эндофункторов, означает, что Compose (частично примененный только к его первым двум параметрам) является ассоциативным, и что Identity является его элементом идентичности. То есть выполняются следующие изоморфизмы:

• Compose f (Compose g h) ~= Compose (Compose f g) h
• Compose f Identity ~= f
• Compose Identity g ~= g

Это очень легко доказать, потому что Compose и Identity оба определены как newtype, а отчеты Haskell определяют семантику newtype как изоморфизм между определяемым типом и типом аргумента конструктора данных newtype. Так, например, давайте докажем Compose f Identity ~= f:

Compose f Identity a
    ~= f (Identity a)                 -- newtype Compose f g a = Compose (f (g a))
    ~= f a                            -- newtype Identity a = Identity a
Q.E.D.

Ответы здесь отлично справляются с определением как моноидов, так и монад, однако, похоже, они все еще не дают ответа на вопрос:

И менее важное замечание: верно ли это, и если да, то не могли бы вы дать объяснение (надеюсь, такое, которое сможет понять тот, кто не имеет большого опыта работы с Haskell)?

Суть вопроса, которого здесь не хватает, - это другое понятие «моноид», так называемая категоризация, точнее, понятие моноида в моноидальной категории. К сожалению, сама книга Мак Лейна

В общем, монада в X - это просто моноид в категории эндофункторов X, где продукт × заменен композицией эндофункторов, а единица задана идентичным эндофунктором.

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

(Строгие) моноидальные категории

Переходя к главе VII о моноидах (которая идет позже, чем глава VI о монадах), мы находим определение так называемой строгой моноидальной категории как тройной (B, *, e), где B - категория, *: B x B-> B a бифунктор (функтор по отношению к каждому компоненту с фиксированным другим компонентом) и e - это единичный объект в B, удовлетворяющий ассоциативности и законам единиц:

(a * b) * c = a * (b * c)
a * e = e * a = a

для любых объектов a,b,c из B, и те же тождества для любых морфизмов a,b,c с e замененным на id_e, морфизм идентичности e. Теперь поучительно заметить, что в нашем интересующем нас случае, где B - категория эндофункторов X с естественными преобразованиями в виде морфизмов, * композиция функторов и e тождественный функтор, все эти законы выполняются, что можно непосредственно проверить.

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

Моноиды в моноидальных категориях

Наконец, в разделе 3 «Моноиды» главы VII дано собственное определение:

Моноид c в моноидальной категории (B, *, e) - это объект B с двумя стрелками (морфизмами)

mu: c * c -> c
nu: e -> c

делая 3 диаграммы коммутативными. Напомним, что в нашем случае это морфизмы в категории эндофункторов, которые являются естественными преобразованиями, соответствующими точно join и return для монады. Связь становится еще яснее, когда мы делаем композицию * более явной, заменяя c * c на c^2, где c - наша монада.

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

Заключение

Таким образом, любая монада по определению является эндофунктором, следовательно, объектом в категории эндофункторов, где монадические операторы join и return удовлетворяют определению моноида в этой конкретной (строгой) моноидальной категории. И наоборот, любой моноид в моноидальной категории эндофункторов по определению является тройкой (c, mu, nu), состоящей из объекта и двух стрелок, например естественные преобразования в нашем случае, удовлетворяющие тем же законам, что и монада.

Наконец, обратите внимание на ключевое различие между (классическими) моноидами и более общими моноидами в моноидальных категориях. Две стрелки mu и nu выше больше не являются двоичной операцией и единицей в наборе. Вместо этого у вас есть один фиксированный эндофунктор c. Сама по себе композиция функторов 52 и тождественный функтор не обеспечивают полной структуры, необходимой для монады, несмотря на это сбивающее с толку замечание в книге.

Другой подход заключался бы в сравнении со стандартным моноидом C всех собственных карт набора A, где двоичная операция представляет собой композицию, которая, как можно видеть, отображает стандартное декартово произведение C x C в C. Переходя к категорированному моноиду, мы заменяем декартово произведение x композицией функторов *, а бинарная операция заменяется естественным преобразованием mu из c * c в c, то есть набором операторов join

join: c(c(T))->c(T)

для каждого объекта T (наберите в программировании). А элементы идентичности в классических моноидах, которые можно идентифицировать с изображениями карт из фиксированного одноточечного набора, заменяются набором операторов return

return: T->c(T) 

Но теперь декартовых произведений больше нет, поэтому нет пар элементов и, следовательно, нет бинарных операций.

Я пришел к этому сообщению, чтобы лучше понять вывод печально известной цитаты из статьи Мак Лейна Теория категорий для рабочего математика.

При описании того, что что-то есть, часто одинаково полезно описать то, чем это не является.

Тот факт, что Мак Лейн использует это описание для описания монады, может означать, что оно описывает нечто уникальное для монад. Потерпите меня. Чтобы развить более широкое понимание этого утверждения, я считаю, что необходимо прояснить, что он не описывает что-то уникальное для монад; это утверждение в равной степени описывает, среди прочего, Applicative и Arrows. По той же причине у нас может быть два моноида на Int (Sum и Product), у нас может быть несколько моноидов на X в категории эндофункторов. Но это еще не все сходство.

И Monad, и Applicative соответствуют критериям:

• endo => любая стрелка или морфизм, который начинается и заканчивается в одном и том же месте
• functor => any arrow, or morphism between two Categories

  (e.g., in day to day Tree a -> List b, but in Category Tree -> List)

• моноид => одиночный объект; т.е. одного типа, но в данном контексте только в отношении внешнего слоя; Итак, у нас не может быть Tree -> List, только List -> List.

The statement uses "Category of..." This defines the scope of the statement. As an example, the Functor Category describes the scope of f * -> g *, i.e., Any functor -> Any functor, e.g., Tree * -> List * or Tree * -> Tree *.

What a Categorical statement does not specify describes where anything and everything is permitted.

In this case, inside the functors, * -> * aka a -> b is not specified which means Anything -> Anything including Anything else. As my imagination jumps to Int -> String, it also includes Integer -> Maybe Int, or even Maybe Double -> Either String Int where a :: Maybe Double; b :: Either String Int.

Итак, утверждение сводится к следующему:

• область действия функтора :: f a -> g b (т. е. от любого параметризованного типа к любому параметризованному типу)
• endo + functor :: f a -> f b (т.е. любой параметризованный тип к одному и тому же параметризованному типу) ... иначе говоря,
• моноид в категории эндофунктора

Итак, в чем же сила этой конструкции? Чтобы оценить всю динамику, мне нужно было увидеть, что типичные рисунки моноида (одиночный объект с тем, что выглядит как стрелка идентичности, :: single object -> single object), не иллюстрируют, что мне разрешено использовать стрелку, параметризованную с помощью любого числа. значений моноида из объекта типа один, разрешенного в Monoid. Определение эквивалентности endo, ~ identity стрелка игнорирует значение типа функтора, а также тип и значение самого внутреннего, "полезного" уровня. Таким образом, эквивалентность возвращает true в любой ситуации, когда совпадают функциональные типы (например, Nothing -> Just * -> Nothing эквивалентно Just * -> Just * -> Just *, потому что они оба Maybe -> Maybe -> Maybe).

Sidebar: ~ outside is conceptual, but is the left most symbol in f a. It also describes what "Haskell" reads-in first (big picture); so Type is "outside" in relation to a Type Value. The relationship between layers (a chain of references) in programming is not easy to relate in Category. The Category of Set is used to describe Types (Int, Strings, Maybe Int etc.) which includes the Category of Functor (parameterized Types). The reference chain: Functor Type, Functor values (elements of that Functor's set, e.g., Nothing, Just), and in turn, everything else each functor value points to. In Category the relationship is described differently, e.g., return :: a -> m a is considered a natural transformation from one Functor to another Functor, different from anything mentioned thus far.

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

• снаружи он выглядит как единый объект (например, :: List); статический
• but inside, permits a lot of dynamics
  • any number of values of the same type (e.g., Empty | ~NonEmpty) as fodder to functions of any arity. The tensor product will reduce any number of inputs to a single value... for the external layer (~fold that says nothing about the payload)
  • бесконечный диапазон и типа и значений для самого внутреннего слоя

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

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

Это часто понимают неправильно. Далее в заявлении join :: m (m a) -> m a описывается как тензорное произведение моноидального эндофунктора. Однако он не формулирует, как в контексте этого утверждения также мог быть выбран (<*>). Это действительно пример шести / полдюжины. Логика объединения значений абсолютно одинакова; один и тот же ввод генерирует одинаковый вывод для каждого (в отличие от моноидов Sum и Product для Int, потому что они генерируют разные результаты при объединении Ints).

Итак, резюмируем: моноид в категории эндофункторов описывает:

   ~t :: m * -> m * -> m *
   and a neutral value for m *

(<*>) и (>>=) оба обеспечивают одновременный доступ к двум значениям m для вычисления единственного возвращаемого значения. Логика, используемая для вычисления возвращаемого значения, точно такая же. Если бы не разные формы параметризируемых ими функций (f :: a -> b по сравнению с k :: a -> m b) и положение параметра с одинаковым типом возвращаемого значения вычисления (т.е. a -> b -> b по сравнению с b -> a -> b для каждого соответственно), я подозреваю, что мы могли бы параметризовать моноидальная логика, тензорное произведение, для повторного использования в обоих определениях. В качестве упражнения, чтобы понять суть, попробуйте реализовать ~t, и вы получите (<*>) и (>>=) в зависимости от того, как вы решите определить его forall a b.

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

В заключение, по моему собственному опыту, печально известная цитата Мак Лейна предоставила мне отличный мем «goto», ориентир, на который я мог ссылаться при навигации по категориям, чтобы лучше понять идиомы, используемые в Haskell. Ему удается охватить объем мощных вычислительных мощностей, которые прекрасно доступны в Haskell.

Однако есть ирония в том, что я сначала неправильно понял применимость утверждения вне монады и то, что, надеюсь, передал здесь. Все, что он описывает, оказывается похожим между Applicative и Monads (и Arrows среди других). Но в нем не говорится о небольшом, но полезном различии между ними.

- E

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

Ниже мой первоначальный ответ.

Вполне возможно, что Ири прочитал От моноидов к монадам, сообщение, в котором Дэн Пипони (sigfpe) извлекает монады из моноидов в Haskell, с подробным обсуждением теории категорий и явным упоминанием «категории эндофункторов на Hask". В любом случае, любой, кто задается вопросом, что значит для монады быть моноидом в категории эндофункторов, может извлечь пользу из прочтения этого вывода.