Was sind freie Monaden?

Question

Ich habe den Begriff Freie Monade auftauchen jede jetzt und dann seit einiger Zeit, aber jeder scheint sie nur zu verwenden/zu diskutieren, ohne zu erklären, was sie sind. Also: Was sind freie Monaden? (Ich würde sagen, ich bin mit Monaden und den Haskell-Grundlagen vertraut, habe aber nur eine sehr grobe Kenntnis der Kategorientheorie).

Answer 1

Hier ist eine noch einfachere Antwort: Eine Monade ist etwas, das "rechnet", wenn der monadische Kontext zusammengebrochen wird durch join :: m (m a) -> m a (unter Hinweis darauf, dass >>= kann definiert werden als x >>= y = join (fmap y x) ). Auf diese Weise tragen Monaden den Kontext durch eine sequentielle Kette von Berechnungen: An jedem Punkt der Reihe wird der Kontext des vorherigen Aufrufs mit dem nächsten zusammengelegt.

A freies Gedankengut erfüllt alle Monadengesetze, führt aber keine Kollabierung (d. h. keine Berechnung) durch. Es wird lediglich eine verschachtelte Reihe von Kontexten aufgebaut. Der Benutzer, der einen solchen freien monadischen Wert erzeugt, ist dafür verantwortlich, etwas mit diesen verschachtelten Kontexten zu tun, so dass die Bedeutung einer solchen Komposition kann aufgeschoben werden, bis der monadische Wert erstellt worden ist.

Answer 2

Die Antwort von Edward Kmett ist natürlich großartig. Aber sie ist ein bisschen technisch. Hier ist eine vielleicht besser verständliche Erklärung.

Freie Monaden sind nur eine allgemeine Möglichkeit, Funktoren in Monaden zu verwandeln. Das heißt, bei einem beliebigen Funktor f Free f ist eine Monade. Dies wäre nicht sehr nützlich, außer man erhält ein Paar von Funktionen

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

Mit der ersten können Sie in Ihre Monade "einsteigen", mit der zweiten können Sie sie "verlassen".

Allgemeiner ausgedrückt: Wenn X ein Y mit einigen zusätzlichen Dingen P ist, dann ist ein "freies X" eine Möglichkeit, von einem Y zu einem X zu gelangen, ohne etwas Zusätzliches zu erhalten.

Beispiele: Ein Monoid (X) ist eine Menge (Y) mit einer zusätzlichen Struktur (P), die im Wesentlichen besagt, dass sie eine Operation (z. B. Addition) und eine Identität (z. B. Null) hat.

Also

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

Nun, wir alle kennen Listen

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

Nun, bei jeder Art von t wir wissen, dass [t] ist ein Monoid

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

und somit sind Listen das "freie Monoid" über Mengen (oder in Haskell Typen).

Okay, freie Monaden sind also die gleiche Idee. Wir nehmen einen Funktor und geben eine Monade zurück. Da Monaden als Monoide in der Kategorie der Endofunktoren betrachtet werden können, ist die Definition einer Liste

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

sieht der Definition von freien Monaden sehr ähnlich

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

und die Monad Instanz hat eine Ähnlichkeit mit der Monoid Instanz für Listen

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

Jetzt erhalten wir unsere beiden Operationen

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

Answer 3

Ein freies foo ist zufällig das einfachste Ding, das alle foo"-Gesetze erfüllt. Das heißt, es erfüllt genau die Gesetze, die notwendig sind, um ein foo zu sein, und nichts darüber hinaus.

Ein vergesslicher Funktor ist ein Funktor, der einen Teil der Struktur "vergisst", wenn er von einer Kategorie in eine andere übergeht.

Gegebene Funktoren F : D -> C y G : C -> D sagen wir F -| G , F ist links adjungiert an G , oder G ist rechts adjungiert an F wann immer forall a, b: F a -> b ist isomorph zu a -> G b , wobei die Pfeile aus den entsprechenden Kategorien stammen.

Formal ist ein freier Funktor links adjungiert zu einem vergesslichen Funktor.

Das freie Monoid

Beginnen wir mit einem einfacheren Beispiel, dem freien Monoid.

Man nehme ein Monoid, das durch eine Trägermenge definiert ist T eine binäre Funktion, um ein Paar von Elementen zusammenzufügen f :: T T T und eine unit :: T so dass man ein Assoziationsgesetz und ein Identitätsgesetz hat: f(unit,x) = x = f(x,unit) .

Sie können einen Funktor erstellen U aus der Kategorie der Monoide (wobei die Pfeile Monoidhomomomorphismen sind, d. h. sie gewährleisten, dass sie unit zu unit auf das andere Monoid, und dass man vor oder nach der Abbildung auf das andere Monoid komponieren kann, ohne die Bedeutung zu ändern) zur Kategorie der Mengen (wo Pfeile nur Funktionspfeile sind), die die Operation "vergisst" und unit und gibt Ihnen nur das Trägerset.

Dann können Sie einen Funktor definieren F von der Kategorie der Mengen zurück zur Kategorie der Monoide, die diesem Funktor links adjungiert ist. Dieser Funktor ist der Funktor, der eine Menge a zum Monoid [a] , wobei unit = [] y mappend = (++) .

Um also unser bisheriges Beispiel in Pseudo-Haskell zu wiederholen:

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

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

Dann zu zeigen F frei ist, müssen wir zeigen, dass sie links adjungiert ist zu U ein vergesslicher Funktor, d. h., wir müssen, wie oben erwähnt, zeigen, dass

F a b ist isomorph zu a U b

Nun, denken Sie an das Ziel von F ist in der Kategorie Mon von Monoiden, wobei die Pfeile Monoidhomomomorphismen sind. Wir brauchen also a, um zu zeigen, dass ein Monoidhomomorphismus von [a] b kann genau durch eine Funktion beschrieben werden, die aus a b .

In Haskell nennen wir die Seite davon, die sich in Set (er, Hask (die Kategorie der Haskell-Typen, von der wir annehmen, dass sie Set ist), einfach foldMap die bei einer Spezialisierung von Data.Foldable to Lists hat den Typ Monoid m => (a m) [a] m .

Die Tatsache, dass es sich um eine Adjunktion handelt, hat Folgen. Vor allem, wenn man vergisst, dann mit free aufbaut und dann wieder vergisst, ist es so, als hätte man es einmal vergessen, und wir können dies nutzen, um die monadische Verbindung aufzubauen. da UFUF ~ U(FUF) ~ UF und wir können den Homomorphismus des Identitätsmonoids von [a] zu [a] durch den Isomorphismus, der unsere Adjunktion definiert, erhalten, dass ein Listenisomorphismus von [a] [a] ist eine Funktion des Typs a -> [a] und das ist nur die Rückgabe für Listen.

Sie können all dies direkter zusammenstellen, indem Sie eine Liste mit diesen Begriffen beschreiben:

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

Die freie Monade

Was also ist ein Freie Monade ?

Wir beginnen mit einem vergesslichen Funktor U von der Kategorie der Monaden, in der die Pfeile Monadenhomomorphismen sind, zu einer Kategorie von Endofunktoren, in der die Pfeile natürliche Transformationen sind, und wir suchen nach einem Funktor, der links adjungiert zu diesem ist.

Was hat das nun mit dem Begriff der freien Monade zu tun, wie er üblicherweise verwendet wird?

Zu wissen, dass etwas eine freie Monade ist, Free f sagt Ihnen, dass ein Monadenhomomorphismus von Free f -> m ist dasselbe (isomorph zu) wie eine natürliche Transformation (ein Funktor-Homomorphismus) von f -> m . Erinnern Sie sich an F a -> b muss isomorph sein zu a -> U b für F, um links adjungiert zu U zu sein. U bildet hier Monaden auf Funktoren ab.

F ist mindestens isomorph zur Free Typ, den ich in meinem free Paket auf hackage.

Wir könnten ihn auch in engerer Analogie zum obigen Code für die freie Liste konstruieren, indem wir definieren

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

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

Cofreie Komonaden

Wir können etwas Ähnliches konstruieren, indem wir das rechte Adjungierte zu einem vergesslichen Funktor betrachten, vorausgesetzt, er existiert. Ein kofreier Funktor ist einfach /rechts adjungiert/ zu einem vergesslichen Funktor, und durch Symmetrie ist das Wissen, dass etwas ein kofreier Komonade ist, dasselbe wie das Wissen, dass es einen Komonadenhomomomorphismus von w -> Cofree f ist das Gleiche wie eine natürliche Umwandlung von w -> f .

Answer 4

Die Freie Monade (Datenstruktur) ist für die Monade (Klasse) wie die Liste (Datenstruktur) für das Monoid (Klasse): Sie ist die triviale Implementierung, bei der man im Nachhinein entscheiden kann, wie der Inhalt kombiniert wird.

---

Sie wissen wahrscheinlich, was eine Monade ist und dass jede Monade eine spezifische (Monadengesetz-konforme) Implementierung von entweder fmap + join + return ou bind + return .

Nehmen wir an, Sie haben einen Functor (eine Implementierung von fmap ), aber der Rest hängt von Werten und Entscheidungen ab, die zur Laufzeit getroffen werden, was bedeutet, dass Sie die Monad-Eigenschaften verwenden können, aber die Monad-Funktionen im Nachhinein auswählen möchten.

Das kann mit der Freien Monade (Datenstruktur) geschehen, die den Functor (Typ) so umhüllt, dass die join ist eher eine Stapelung dieser Funktoren als eine Reduktion.

Die echte return et join die Sie verwenden möchten, können nun als Parameter an die Reduktionsfunktion übergeben werden foldFree :

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

Um die Typen zu erklären, können wir Folgendes ersetzen Functor f con Monad m et b con (m a) :

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

Answer 5

Eine freie Monade in Haskell ist eine Liste von Funktoren. Vergleiche:

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

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

Pure ist analog zu Nil et Free ist analog zu Cons . Eine freie Monade speichert eine Liste von Funktoren anstelle einer Liste von Werten. Technisch gesehen könnte man freie Monaden auch mit einem anderen Datentyp implementieren, aber jede Implementierung sollte isomorph zu der obigen sein.

Sie verwenden freie Monaden, wenn Sie einen abstrakten Syntaxbaum benötigen. Der Basisfunktor der freien Monade ist die Form der einzelnen Stufen des Syntaxbaums.

Mein Beitrag die jemand bereits verlinkt hat, gibt mehrere Beispiele dafür, wie man abstrakte Syntaxbäume mit freien Monaden aufbauen kann