Que sont les monades gratuites?

Je l' ai vu le terme gratuit Monad pop - up chaque maintenant et puis pendant un certain temps, mais tout le monde semble juste d'utiliser / en discuter sans donner une explication de ce qu'ils sont. Alors: que sont les monades gratuites? (Je dirais que je connais les monades et les bases de Haskell, mais que je n'ai qu'une connaissance très approximative de la théorie des catégories.)

La réponse d'Edward Kmett est évidemment excellente. Mais c'est un peu technique. Voici une explication peut-être plus accessible.

Les monades gratuites ne sont qu'un moyen général de transformer des foncteurs en monades. Autrement dit, étant donné que tout foncteur f Free fest une monade. Ce ne serait pas très utile, sauf si vous obtenez une paire de fonctions

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

le premier vous permet de "rentrer" dans votre monade, et le second vous donne un moyen de "sortir" de celle-ci.

Plus généralement, si X est un Y avec quelques trucs supplémentaires P, alors un "X libre" est un moyen de passer d'un Y à un X sans rien gagner de plus.

Exemples: un monoïde (X) est un ensemble (Y) avec une structure supplémentaire (P) qui dit essentiellement qu'il a une opération (vous pouvez penser à l'addition) et une certaine identité (comme zéro).

Donc

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

Maintenant, nous connaissons tous des listes

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

Eh bien, étant donné tout type, tnous savons que [t]c'est un monoïde

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

et ainsi les listes sont le "monoïde libre" sur les ensembles (ou dans les types Haskell).

D'accord, donc les monades gratuites sont la même idée. Nous prenons un foncteur et rendons une monade. En fait, comme les monades peuvent être considérées comme des monoïdes dans la catégorie des endofoncteurs, la définition d'une liste

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

ressemble beaucoup à la définition des monades libres

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

et l' Monadinstance a une similitude avec l' Monoidinstance pour les listes

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

maintenant, nous obtenons nos deux opérations

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

Voici une réponse encore plus simple: Une Monade est quelque chose qui "calcule" lorsque le contexte monadique est réduit par join :: m (m a) -> m a(rappelant que cela >>=peut être défini comme x >>= y = join (fmap y x)). C'est ainsi que les Monades transportent le contexte à travers une chaîne séquentielle de calculs: car à chaque point de la série, le contexte de l'appel précédent est réduit au suivant.

Une monade libre satisfait à toutes les lois de la monade, mais ne fait pas d'effondrement (c.-à-d. Calcul). Il crée simplement une série de contextes imbriqués. L'utilisateur qui crée une telle valeur monadique libre est responsable de faire quelque chose avec ces contextes imbriqués, de sorte que la signification d'une telle composition puisse être différée jusqu'à ce que la valeur monadique ait été créée.

Un foo gratuit se trouve être la chose la plus simple qui satisfait toutes les lois du foo. C'est-à-dire qu'il satisfait exactement aux lois nécessaires pour être un fou et rien de plus.

Un foncteur oublieux est celui qui «oublie» une partie de la structure en passant d'une catégorie à l'autre.

Des foncteurs donnés F : D -> C, et G : C -> D, disons-nous F -| G, Fsont adjoints à gauche Gou Gsont adjoints à droite Fchaque fois que tout a, b: F a -> best isomorphe à a -> G b, où les flèches proviennent des catégories appropriées.

Formellement, un foncteur libre est laissé adjoint à un foncteur oublieux.

Le monoïde gratuit

Commençons par un exemple plus simple, le monoïde libre.

Prenez un monoïde, qui est défini par un ensemble de support T, une fonction binaire pour écraser une paire d'éléments ensemble f :: T → T → T, et unit :: T, de sorte que vous avez une loi associative, et une loi d'identité: f(unit,x) = x = f(x,unit).

Vous pouvez créer un foncteur à Upartir de la catégorie des monoïdes (où les flèches sont des homomorphismes monoïdes, c'est-à-dire qu'ils s'assurent qu'ils correspondent unità unitl'autre monoïde et que vous pouvez composer avant ou après le mappage à l'autre monoïde sans changer de signification) à la catégorie d'ensembles (où les flèches ne sont que des flèches de fonction) qui «oublie» l'opération et unit, et vous donne simplement l'ensemble de support.

Ensuite, vous pouvez définir un foncteur Fde la catégorie des ensembles à la catégorie des monoïdes qui reste adjointe à ce foncteur. Ce foncteur est le foncteur qui associe un ensemble aau monoïde [a], où unit = []et mappend = (++).

Donc, pour passer en revue notre exemple jusqu'à présent, en pseudo-Haskell:

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

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

Ensuite, pour montrer que Fc'est gratuit, nous devons démontrer qu'il est laissé adjoint à U, un foncteur oublieux, c'est-à-dire, comme nous l'avons mentionné ci-dessus, nous devons montrer que

F a → b est isomorphe à a → U b

maintenant, rappelez-vous que la cible de Fest dans la catégorie Mondes monoïdes, où les flèches sont des homomorphismes monoïdes, nous avons donc besoin d'un pour montrer qu'un homomorphisme monoïde de [a] → bpeut être décrit précisément par une fonction de a → b.

Dans Haskell, nous appelons le côté de cela qui vit dans Set(euh, Haskla catégorie de types Haskell que nous prétendons être Set), juste foldMap, qui, lorsqu'elle est spécialisée de Data.Foldableà Lists, a du type Monoid m => (a → m) → [a] → m.

Il y a des conséquences qui découlent de cette adjonction. Notamment, si vous oubliez, puis construisez avec free, puis oubliez à nouveau, c'est comme vous l'avez oublié une fois, et nous pouvons l'utiliser pour construire la jointure monadique. depuis UFUF~ U(FUF)~ UF, et nous pouvons passer dans l'homomorphisme monoïde d'identité de [a]à [a]travers l'isomorphisme qui définit notre adjonction, obtenir qu'un isomorphisme de liste [a] → [a]est une fonction de type a -> [a], et c'est juste un retour pour les listes.

Vous pouvez composer tout cela plus directement en décrivant une liste en ces termes avec:

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

La monade libre

Qu'est-ce qu'une Free Monad ?

Eh bien, nous faisons la même chose que nous faisions avant, nous commençons avec un foncteur oublieux U de la catégorie des monades où les flèches sont des homomorphismes de monade à une catégorie d'endofoncteurs où les flèches sont des transformations naturelles, et nous recherchons un foncteur qui est laissé adjoint pour que.

Alors, comment cela se rapporte-t-il à la notion de monade libre telle qu'elle est généralement utilisée?

Savoir que quelque chose est une monade libre, Free fvous dit que donner un homomorphisme de monade à partir de Free f -> m, c'est la même chose (isomorphe à) que donner une transformation naturelle (un homomorphisme de foncteur) à partir de f -> m. Rappelez-vous que F a -> bdoit être isomorphe pour a -> U bque F soit laissé adjoint à U. U ici mappé des monades aux foncteurs.

F est au moins isomorphe au Freetype que j'utilise dans mon freepackage sur le piratage.

Nous pourrions également le construire dans une analogie plus étroite avec le code ci-dessus pour la liste gratuite, en définissant

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

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

Cofree Comonads

Nous pouvons construire quelque chose de similaire, en regardant l'adjoint de droite d'un foncteur oublieux en supposant qu'il existe. Un foncteur cofree est simplement / à droite adjoint / à un foncteur oublieux, et par symétrie, savoir que quelque chose est un comonad cofree revient à savoir que donner un homomorphisme comonad à partir de w -> Cofree fest la même chose que donner une transformation naturelle à partir de w -> f.

La Free Monad (structure de données) est à la Monad (classe) comme la List (structure de données) à Monoid (classe): c'est l'implémentation triviale, où vous pouvez décider ensuite comment le contenu sera combiné.

Vous savez probablement ce qu'est une Monade et que chaque Monade a besoin d'une implémentation spécifique (respectant la loi de la Monade) de fmap+ join+ returnou bind+ return.

Supposons que vous ayez un Functor (une implémentation de fmap) mais le reste dépend des valeurs et des choix effectués au moment de l'exécution, ce qui signifie que vous voulez pouvoir utiliser les propriétés Monad mais que vous souhaitez choisir les fonctions Monad par la suite.

Cela peut être fait en utilisant la Free Monad (structure de données), qui enveloppe le Functor (type) de manière à ce que ce joinsoit plutôt un empilement de ces foncteurs qu'une réduction.

Le réel returnet celui que joinvous souhaitez utiliser peuvent désormais être donnés comme paramètres à la fonction de réduction foldFree:

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

Pour expliquer les types, nous pouvons remplacer Functor fpar Monad met bpar (m a):

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

Une monade libre Haskell est une liste de foncteurs. Comparer:

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

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

Pureest analogue à Nilet Freeest analogue à Cons. Une monade gratuite stocke une liste de foncteurs au lieu d'une liste de valeurs. Techniquement, vous pouvez implémenter des monades gratuites en utilisant un type de données différent, mais toute implémentation doit être isomorphe à celle ci-dessus.

Vous utilisez des monades gratuites chaque fois que vous avez besoin d'un arbre de syntaxe abstrait. Le foncteur de base de la monade libre est la forme de chaque étape de l'arbre de syntaxe.

Mon article , que quelqu'un a déjà lié, donne plusieurs exemples de la façon de construire des arbres de syntaxe abstraits avec des monades gratuites

Je pense qu'un simple exemple concret sera utile. Supposons que nous ayons un foncteur

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

avec l'évidence fmap. Ensuite , Free F aest le type d'arbres dont les feuilles ont le type aet dont les noeuds sont étiquetés avec One, Two, Two'et Three. One-les nœuds ont un enfant,Two - et Two'-nodes ont deux enfants et Three-nodes en ont trois et sont également étiquetés avec un Int.

Free Fest une monade. returncorrespond xà l'arbre qui n'est qu'une feuille avec une valeurx . t >>= fregarde chacune des feuilles et les remplace par des arbres. Lorsque la feuille a une valeur, yelle remplace cette feuille par l'arbre f y.

Un diagramme rend cela plus clair, mais je n'ai pas les moyens d'en dessiner facilement un!