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

Ответ 1

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

Свободные монады - это просто общий способ превращения функторов в монады. То есть, если любой функтор 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)

Ответ 2

Здесь еще более простой ответ: Monad - это то, что "вычисляет", когда монадический контекст свернут с помощью join :: m (ma) → ma (напоминая, что >>= можно определить как x >>= y = join (fmap yx)). Вот как монады переносят контекст через последовательную цепочку вычислений: потому что в каждой точке ряда контекст предыдущего вызова свернут со следующим.

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

Ответ 3

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

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

Учитывая функторы F : D -> C и G : C -> D, мы говорим F -| G, F присоединяется слева к G, или G присоединяется справа к F всякий раз, когда forall 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.Foldable до Lists, имеет тип 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. 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)

Cofree Comonads

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

Ответ 4

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

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

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

Это можно сделать, используя Free Monad (структура данных), которая обертывает Functor (type) таким образом, чтобы 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)

Ответ 5

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

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

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

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

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

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

Ответ 6

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

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 -ноды имеют один дочерний элемент, Two - и Two' -ноды имеют два дочерних элемента и Three -ноды имеют три и также помечены знаком Int.

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

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