Что такое свободные монады?
Я видел термин Свободные Монады поп теперьизатем в течение некоторого времени, но все просто используют/обсуждают их, не давая объяснения того, что они есть. Итак: что такое свободные монады? (Я бы сказал, что знаком с монадами и основами Хаскелла, но имею только очень грубое знание теории категорий.)
6 ответов:
Эдвард Kmett явно велика. Но, это немного технически. Вот, пожалуй, более доступное объяснение.
свободные монады-это просто общий способ превращения функторов в монады. То есть, учитывая любой функтор
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
(ссылаясь, что>>=
можно определить как(join .) . flip fmap
). Вот как монады переносят контекст через последовательную цепочку вычислений: потому что в каждой точке серии контекст из предыдущего вызова сворачивается со следующим.A свободные монады удовлетворяет всем законам монады, но не рушится (т. е. расчет). Это просто создает вложенный ряд контекстов. Пользователь, который создает такое свободное монадическое значение, отвечает за выполнение чего-то с этими вложенными контекстами, так что смысл такая композиция может быть отложена до тех пор, пока не будет создано монадическое значение.
свободный фу оказывается самой простой вещью, которая удовлетворяет всем законам "фу". То есть он точно удовлетворяет законам, необходимым для того, чтобы быть foo и ничего лишнего.
забывчивый функтор-это тот, который" забывает " часть структуры, когда она переходит из одной категории в другую.
учитывая функторы
F : D -> C
иG : C -> D
, мы говоримF -| G
,F
слева примыкает кG
илиG
справа примыкает кF
всякий раз, когда forall a, b:F a -> b
is изоморфно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
.в Хаскелле мы называем сторону этого, которая живет в
Set
(РП,Hask
, категория типов Haskell, которые мы притворяемся Комплект), простоfoldMap
, который при специализации отData.Foldable
к спискам имеет типMonoid m => (a → m) → [a] → m
.есть последствия, которые вытекают из того, что это примыкание. Примечательно, что если вы забудете, то создадите free, а затем снова забудете, так же, как вы забыли один раз, и мы можем использовать это для создания монадического соединения. так как
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
пакет на hackage.мы также могли бы построить его в более жесткой аналогии с кодом выше для свободного списка, определив
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
.
Свободная Монада (структура данных) относится к монаде (классу), как список (структура данных) к Моноиду (классу): это тривиальная реализация, где вы можете впоследствии решить, как будет объединено содержимое.
вы, наверное, знаете, что такое Монада и что каждая Монада нуждается в конкретной (Монада-законопослушный) реализации либо
fmap
+join
+return
илиbind
+return
.предположим, что у вас есть функтор (реализация
fmap
) но остальное зависит от значений и выбора, сделанных во время выполнения, что означает, что вы хотите иметь возможность использовать свойства монады, но хотите выбрать функции монады после этого.это можно сделать с помощью свободной монады (структуры данных), которая обертывает функтор (тип) таким образом, что
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)
свободная монада Хаскелла-это список функторов. Сравните:
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
-узлы имеют одного ребенка,Two
иTwo'
-узлы имеют двух детей иThree
-узлы имеют три и также с меткойInt
.
Free F
- это монада.return
картыx
к дереву, которое является просто листом со значениемx
.t >>= f
смотрит на каждый из листьев и заменяет их деревьями. Когда лист имеет значениеy
он заменяет этот лист деревомf y
.диаграмма делает это более ясным, но у меня нет средств для легкого рисования!