Co to są darmowe monady?

Widziałem termin Monada bezpłatny pojawiają się za każdym teraz i potem przez jakiś czas, ale wszyscy po prostu wydaje się używać / omówić je bez podania wyjaśnienia, jakie są. Czym są darmowe monady? (Powiedziałbym, że jestem zaznajomiony z monadami i podstawami Haskella, ale mam tylko bardzo przybliżoną wiedzę na temat teorii kategorii.)

Odpowiedź Edwarda Kmetta jest oczywiście świetna. Ale to jest trochę techniczne. Oto być może bardziej przystępne wyjaśnienie.

Darmowe monady to tylko ogólny sposób na przekształcenie funktorów w monady. To znaczy, biorąc pod uwagę, że każdy funktor f Free fjest monadą. Nie byłoby to bardzo przydatne, z wyjątkiem pary funkcji

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

pierwszy z nich pozwala „dostać się” do monady, a drugi umożliwia „wydostanie się” z niej.

Mówiąc bardziej ogólnie, jeśli X to Y z dodatkowymi dodatkami P, to „wolny X” jest sposobem na przejście od Y do X bez uzyskiwania czegoś dodatkowego.

Przykłady: monoid (X) to zbiór (Y) z dodatkową strukturą (P), który w zasadzie mówi, że ma operację (możesz pomyśleć o dodaniu) i pewną tożsamość (jak zero).

Więc

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

Teraz wszyscy znamy listy

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

Cóż, biorąc pod uwagę każdy typ, tktóry wiemy, że [t]jest monoidem

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

dlatego listy są „wolnymi monoidami” nad zestawami (lub w typach Haskella).

Okej, więc wolne monady to ten sam pomysł. Bierzemy funktor i oddajemy monadę. W rzeczywistości, ponieważ monady można postrzegać jako monoidy w kategorii endofunkcji, definicja listy

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

wygląda bardzo podobnie do definicji wolnych monad

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

i Monadinstancja ma podobieństwo do Monoidinstancji dla list

--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

teraz mamy dwie operacje

-- 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)

Oto jeszcze prostsza odpowiedź: monada jest czymś, co „oblicza się”, gdy kontekst monadyczny jest zwinięty join :: m (m a) -> m a(przypominając, że >>=można to zdefiniować jako x >>= y = join (fmap y x)). W ten sposób Monady przenoszą kontekst przez sekwencyjny łańcuch obliczeń: ponieważ w każdym punkcie serii kontekst z poprzedniego wywołania jest zawijany do następnego.

A darmowe Monad spełnia wszystkie ustawowe Monad, ale nie robi żadnego zawaleniem (tj obliczeń). Po prostu tworzy zagnieżdżoną serię kontekstów. Użytkownik, który tworzy taką wolną wartość monadyczną, jest odpowiedzialny za zrobienie czegoś z tymi zagnieżdżonymi kontekstami, tak aby znaczenie takiej kompozycji można było odłożyć do momentu utworzenia wartości monadycznej.

Bezpłatne foo okazuje się najprostszą rzeczą, która spełnia wszystkie prawa „foo”. To znaczy, że spełnia dokładnie prawa niezbędne do bycia foo i nic więcej.

Zapominający funktor to taki, który „zapomina” część struktury, przechodząc z jednej kategorii do drugiej.

Biorąc pod uwagę funktory F : D -> C, i G : C -> D, jak mówimy F -| G, Fjest on przyległy do G, lub Gjest przyległy do, Filekroć forall a, b: F a -> bjest izomorficzny a -> G b, gdzie strzałki pochodzą z odpowiednich kategorii.

Formalnie wolny funktor pozostaje przyległy do ​​zapomnianego funktora.

Wolny Monoid

Zacznijmy od prostszego przykładu, wolnej monoidy.

Weź monoid, który jest zdefiniowany przez jakiś zestaw nośnej T, funkcja binarna mash parę elementów ze sobą f :: T → T → T, a także unit :: Ttakie, które mają prawo zrzeszania się, prawo oraz tożsamości: f(unit,x) = x = f(x,unit).

Możesz zrobić funktor Uz kategorii monoidów (gdzie strzałki są homomorfizmami monoidów, tzn. Zapewniają, że odwzorowują unitsię unitna innym monoidie, i że możesz komponować przed lub po mapowaniu na drugą monoidę bez zmiany znaczenia) do kategorii zestawów (gdzie strzałki są tylko strzałkami funkcyjnymi), które „zapominają” o operacji uniti po prostu dają ci zestaw nośny.

Następnie możesz zdefiniować funktor Fz kategorii zestawów z powrotem do kategorii monoidów, która pozostaje przyległa do tego funktora. Ten funktor jest funktorem, który odwzorowuje zbiór ana monoid [a], gdzie unit = []i mappend = (++).

Aby przejrzeć nasz dotychczasowy przykład w pseudo-Haskell:

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

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

Następnie pokazanie Fjest bezpłatne, musimy wykazać, że jest on sąsiadujący z Uzapomnianym funktorem, to znaczy, jak wspomniano powyżej, musimy pokazać, że

F a → b jest izomorficzny a → U b

pamiętajcie teraz, że cel Fjest w kategorii Monmonoidów, gdzie strzały są homomorfizmami monoidów, więc musimy pokazać, że homomorfizm monoidów z [a] → bmożna dokładnie opisać funkcją a → b.

W Haskell nazywamy stronę tego, w której żyjemy Set(er, Haskkategoria typów Haskell, którą udajemy, jest ustawiona), właśnie foldMap, która, gdy specjalizujemy Data.Foldablesię w Listach, ma typ Monoid m => (a → m) → [a] → m.

Istnieją konsekwencje wynikające z tego, że jest to dodatek. Zwłaszcza, że ​​jeśli zapomnisz, a następnie zbuduj za darmo, to zapomnij jeszcze raz, tak jak raz zapomniałeś, a my możemy to wykorzystać do zbudowania połączenia monadycznego. ponieważ UFUF~ U(FUF)~ UF, i możemy przekazać tożsamość monomorfizmu monoidu od [a]do [a]poprzez izomorfizm, który określa nasze przyleganie, uzyskajmy, że izomorfizm listy od [a] → [a]jest funkcją typu a -> [a], a to jest po prostu powrót do list.

Możesz to wszystko skomponować bardziej bezpośrednio, opisując listę w tych kategoriach za pomocą:

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

Wolna monada

Czym jest wolna monada ?

Cóż, robimy to samo, co poprzednio, zaczynamy od zapomnianego funktora U z kategorii monad, w których strzały są homomorfizmami monad, do kategorii endofunkcji, w których strzały są naturalnymi transformacjami, i szukamy funktora, który jest pozostawiony obok siebie do tego.

Jak to się ma do pojęcia wolnej monady, jak się zwykle używa?

Wiedząc, że coś jest wolną monadą, Free fmówi ci, że nadanie monomorfizmowi monady z Free f -> m, jest tym samym (izomorficznym), co nadanie naturalnej transformacji (homomorfizm funktorski) f -> m. Pamiętaj, że F a -> bmusi być izomorficzny, aby a -> U bF pozostawał przyległy do ​​U. U tutaj mapowane monady na funktory.

F jest co najmniej izomorficzny do Freetypu używanego w moim freepakiecie podczas włamań.

Możemy również skonstruować go w ścisłej analogii do powyższego kodu dla wolnej listy, definiując

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

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

Cofree Comonady

Możemy skonstruować coś podobnego, patrząc na właściwe połączenie z zapomnianym funktorem, zakładając, że istnieje. Funktor Cofree jest po prostu / właściwie przylegający / do zapomnianego funktora, a symetria, wiedząc, że coś jest cofree comonad, jest tym samym, co wiedza, że ​​nadanie homomorfizmu comonad z w -> Cofree fjest tym samym, co danie naturalnej transformacji w -> f.

Free Monad (struktura danych) odnosi się do Monady (klasy), podobnie jak List (struktura danych) do Monoid (klasy): Jest to trywialna implementacja, w której możesz później zdecydować, w jaki sposób zawartość zostanie połączona.

Prawdopodobnie wiesz, czym jest Monada i że każda Monada potrzebuje specyficznej (zgodnej z prawem Monady) implementacji fmap+ join+ returnlub bind+ return.

Załóżmy, że masz Functor (implementacja fmap), ale reszta zależy od wartości i wyborów dokonanych w czasie wykonywania, co oznacza, że ​​chcesz móc korzystać z właściwości Monady, ale później wybrać funkcje Monady.

Można tego dokonać za pomocą Free Monad (struktura danych), która otacza Functor (typ) w taki sposób, że joinjest to raczej układanie tych funktorów niż redukcja.

Rzeczywiste returni joinchcesz użyć, można teraz podać jako parametry funkcji redukcji foldFree:

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

Aby wyjaśnić rodzajów, możemy wymienić Functor fz Monad moraz bz (m a):

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

Monada wolna od Haskella to lista funktorów. Porównać:

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

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

Purejest analogiczny do Nili Freejest analogiczny do Cons. Wolna monada przechowuje listę funktorów zamiast listy wartości. Technicznie rzecz biorąc, możesz implementować wolne monady przy użyciu innego typu danych, ale każda implementacja powinna być izomorficzna do powyższej.

Korzystasz z bezpłatnych monad, gdy potrzebujesz abstrakcyjnego drzewa składni. Podstawowym funktorem wolnej monady jest kształt każdego kroku drzewa składniowego.

Mój post , który ktoś już powiązał, podaje kilka przykładów, jak budować abstrakcyjne drzewa składniowe za pomocą wolnych monad

Myślę, że prosty konkretny przykład pomoże. Załóżmy, że mamy funktor

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

z oczywistym fmap. Wtedy Free F ajest rodzaj drzew, których liście mają rodzaj ai której węzły są otagowane One, Two, Two'i Three. One-nodes mają jedno dziecko, Two- i Two'-nodes mają dwa dzieci, a Three-nodes ma trzy i są również oznaczone tagiem Int.

Free Fjest monadą. returnmapuje xna drzewo, które jest tylko liściem o wartości x. t >>= fpatrzy na każdy z liści i zastępuje je drzewami. Gdy liść ma wartość y, zastępuje ten liść drzewem f y.

Schemat czyni to jaśniejszym, ale nie mam możliwości łatwego narysowania jednego!