Что такое бесплатные монады?

Я видел этот термин Free Монада всплывал каждый в настоящее время , и затем в течение некоторого времени, но каждый раз кажется , что использование / обсуждать их , не давая объяснение того , что они есть. Итак: что такое бесплатные монады? (Я бы сказал, что я знаком с монадами и основами Хаскелла, но имею только очень грубые знания теории категорий.)

Ответ Эдварда Кметта, очевидно, великолепен. Но это немного технический. Вот, пожалуй, более доступное объяснение.

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

liftFree :: Functor f => f a -> Free f a
foldFree :: Functor f => (f r -> r) -> Free f r -> r

первый из них позволяет вам «войти» в вашу монаду, а второй - как «выйти» из нее.

В более общем смысле, если X - это Y с некоторыми дополнительными элементами P, то «свободный X» - это способ перехода от Y к X без получения чего-либо дополнительного.

Примеры: моноид (X) - это набор (Y) с дополнительной структурой (P), который в основном говорит, что у него есть операция (вы можете думать о сложении) и некоторая идентичность (например, ноль).

Так

class Monoid m where
   mempty  :: m
   mappend :: m -> m -> m

Теперь мы все знаем списки

data [a] = [] | a : [a]

Ну, учитывая любой тип, tмы знаем, что [t]это моноид

instance Monoid [t] where
  mempty   = []
  mappend = (++)

и поэтому списки являются «свободным моноидом» над наборами (или в типах Haskell).

Итак, бесплатные монады - это та же идея. Мы берем функтор и возвращаем монаду. Фактически, поскольку монады можно рассматривать как моноиды в категории эндофункторов, определение списка

data [a] = [] | a : [a]

очень похоже на определение свободных монад

data Free f a = Pure a | Roll (f (Free f a))

и Monadэкземпляр имеет сходство с Monoidэкземпляром для списков

--it needs to be a functor
instance Functor f => Functor (Free f) where
  fmap f (Pure a) = Pure (f a)
  fmap f (Roll x) = Roll (fmap (fmap f) x)

--this is the same thing as (++) basically
concatFree :: Functor f => Free f (Free f a) -> Free f a
concatFree (Pure x) = x
concatFree (Roll y) = Roll (fmap concatFree y)

instance Functor f => Monad (Free f) where
  return = Pure -- just like []
  x >>= f = concatFree (fmap f x)  --this is the standard concatMap definition of bind

теперь мы получаем две наши операции

-- this is essentially the same as \x -> [x]
liftFree :: Functor f => f a -> Free f a
liftFree x = Roll (fmap Pure x)

-- this is essentially the same as folding a list
foldFree :: Functor f => (f r -> r) -> Free f r -> r
foldFree _ (Pure a) = a
foldFree f (Roll x) = f (fmap (foldFree f) x)

Вот еще более простой ответ: Монада - это то, что «вычисляется», когда монадический контекст разрушается join :: m (m a) -> m a(напоминая, что >>=это можно определить как x >>= y = join (fmap y x)). Вот как монады переносят контекст через последовательную цепочку вычислений: потому что в каждой точке ряда контекст предыдущего вызова свернут со следующим.

А свободная монада удовлетворяет все законы Монады, но не делают какое - либо рушится (то есть вычисление). Он просто создает вложенную серию контекстов. Пользователь, который создает такое бесплатное монадическое значение, отвечает за то, чтобы что-то делать с этими вложенными контекстами, так что значение такой композиции может быть отложено до тех пор, пока монадное значение не будет создано.

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

Забывчивый функтор - это тот, кто «забывает» часть структуры при переходе из одной категории в другую.

Данные функторы F : D -> C, и G : C -> D, мы говорим F -| G, Fприсоединены слева Gили Gприсоединены справа к Fвсякий раз, когда все a, b: F a -> bизоморфно a -> G b, где стрелки приходят из соответствующих категорий.

Формально свободный функтор оставляется присоединенным к забывчивому функтору.

Свободный моноид

Давайте начнем с более простого примера - свободного моноида.

Возьмите моноид, который определяется некоторым набором носителей T, бинарная функция помять пару элементов вместе f :: T → T → T, и unit :: T, таким образом, что у вас есть ассоциативный закон, и закон идентичности: f(unit,x) = x = f(x,unit).

Вы можете сделать функтор Uиз категории моноидов (где стрелки являются моноидными гомоморфизмами, то есть они гарантируют, что они сопоставляются unitс unitдругим моноидом, и что вы можете создавать до или после сопоставления с другим моноидом без изменения значения) в категорию наборов (где стрелки - просто функциональные стрелки), которые «забывают» об операции и unit, и просто дают вам набор несущих.

Затем вы можете определить функтор Fиз категории множеств обратно в категорию моноидов, оставленных присоединенными к этому функтору. Этот функтор является функтором, который отображает набор aв моноид [a], где unit = []и mappend = (++).

Итак, чтобы рассмотреть наш пример до сих пор, в псевдо-Haskell:

U : Mon → Set -- is our forgetful functor
U (a,mappend,mempty) = a

F : Set → Mon -- is our free functor
F a = ([a],(++),[])

Затем, чтобы показать, что Fэто бесплатно, мы должны продемонстрировать, что он оставлен присоединенным к Uзабывчивому функтору, то есть, как мы упоминали выше, нам нужно показать, что

F a → b изоморфен a → U b

помните, что цель Fнаходится в категории Monмоноидов, где стрелки являются моноидными гомоморфизмами, поэтому нам нужно показать, что гомоидизм моноидов из [a] → bможет быть точно описан функцией из a → b.

В Haskell мы называем ту сторону этого, которая живет в Set(то есть, Haskкатегория типов Haskell, которую мы притворяемся, это Set), просто foldMap, которая, когда специализируется от Data.FoldableLists, имеет тип Monoid m => (a → m) → [a] → m.

Из этого следствия вытекают последствия. Примечательно, что если вы забудете, то создайте бесплатно, а затем снова забудете, это так же, как вы однажды забыли, и мы можем использовать это для создания монадического соединения. так как UFUF~ U(FUF)~ UF, и мы можем перейти в тождестве моноидного гомоморфизма [a]с [a]помощью изоморфизма , который определяет наше примыкание, получаю , что список изоморфизмомом [a] → [a]является функцией типа a -> [a], и это просто вернуться к спискам.

Вы можете составить все это более непосредственно, описав список в следующих терминах:

newtype List a = List (forall b. Monoid b => (a -> b) -> b)

Свободная Монада

Так что же такое свободная монада ?

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

Итак, как это относится к понятию свободной монады, как это обычно используется?

Знание того, что что-то является свободной монадой, Free fговорит вам, что дать гомоморфизм монады из Free f -> m, это то же самое (изоморфно), что и дать естественное преобразование (гомоморфизм функторов) из f -> m. Помните, что он F a -> bдолжен быть изоморфным для того, a -> U bчтобы F оставался присоединенным к U. Здесь монады отображаются на функторы.

F, по крайней мере, изоморфен Freeтипу, который я использую в моем freeпакете при взломе.

Мы могли бы также построить его в более тесной аналогии с приведенным выше кодом для свободного списка, определив

class Algebra f x where
  phi :: f x -> x

newtype Free f a = Free (forall x. Algebra f x => (a -> x) -> x)

Кофейные Комонады

Мы можем построить нечто подобное, взглянув на правое сопряжение с забывчивым функтором, предполагая, что оно существует. Свободный функтор просто / прямо присоединен / к забывчивому функтору, и симметрично знать, что что-то является свободной комонадой, - это то же самое, что знать, что давать гомоморфизм комонады из w -> Cofree f- это то же самое, что давать естественное преобразование из w -> f.

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

Вы , наверное , знаете , что такое Монада и что каждая Монада нуждается в конкретных (Monad-законопослушные) осуществление любой fmap+ join+ returnили bind+ return.

Предположим, у вас есть Functor (реализация fmap), но все остальное зависит от значений и выборов, сделанных во время выполнения, что означает, что вы хотите иметь возможность использовать свойства Monad, но затем хотите выбрать функции Monad.

Это можно сделать с помощью Free Monad (структура данных), которая оборачивает Functor (тип) таким образом, что joinэто скорее сложение этих функторов, чем сокращение.

Реальное returnи которое joinвы хотите использовать, теперь могут быть заданы в качестве параметров функции сокращения foldFree:

foldFree :: Functor f => (a -> b) -> (f b -> b) -> Free f a -> b
foldFree return join :: Monad m => Free m a -> m a

Чтобы объяснить типы, мы можем заменить Functor fна Monad mи bна (m a):

foldFree :: Monad m => (a -> (m a)) -> (m (m a) -> (m a)) -> Free m a -> (m a)

Свободная монада Haskell - это список функторов. Для сравнения:

data List a   = Nil    | Cons  a (List a  )

data Free f r = Pure r | Free (f (Free f r))

Pureаналогично Nilи Freeаналогично Cons. Бесплатная монада хранит список функторов вместо списка значений. Технически, вы можете реализовать бесплатные монады, используя другой тип данных, но любая реализация должна быть изоморфна вышеупомянутой.

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

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

Я думаю, что простой конкретный пример поможет. Предположим, у нас есть функтор

data F a = One a | Two a a | Two' a a | Three Int a a a

с очевидным fmap. Тогда Free F aтип деревьев, листья которых имеют тип aи чьи узлы помечены One, Two, Two'и Three. Oneузлы -nodes имеют одного дочернего элемента, Twoа Two'узлы -no имеют двух дочерних Threeузлов, а узлы -no имеют три дочерних элемента и также помечаются знаком Int.

Free Fэто монада returnотображается xна дерево, которое является просто листом со значением x. t >>= fсмотрит на каждое из листьев и заменяет их деревьями. Когда лист имеет значение, yон заменяет этот лист деревом f y.

Диаграмма делает это более понятным, но у меня нет возможности легко ее нарисовать!