Quelles sont gratuit monades?

Question

J'ai vu le terme Libre Monade pop up de chaque maintenant et puis pour un certain temps, mais tout le monde semble utiliser/discuter sans donner une explication de ce qu'ils sont. Donc: ce sont libre monades? (Je dirais que je suis familier avec les monades et les Haskell notions de base, mais ont seulement une connaissance très approximative de la catégorie de la théorie.)

Answer 1

Voici un moyen encore plus simple de répondre: Une Monade est quelque chose qui "calcule" quand monadique contexte est effondré join :: m (m a) -> m a (en rappelant qu' >>= peut être définie comme (join .) . flip fmap). C'est de cette façon Monades réaliser en contexte séquentiel de la chaîne de calculs: parce que, à chaque point de la série, le contexte de l'appel précédent est effondré avec le suivant.

Un gratuit monade répond à toutes les Monade des lois, mais ne pas faire s'effondrer (c'est à dire, les calculs). Il a juste construit un imbriquée série de contextes. L'utilisateur qui crée un tel gratuit monadique valeur est responsable de faire quelque chose avec ces contextes imbriqués, de sorte que le sens d'une telle composition peut être reporté jusqu'à ce que la valeur monadique a été créé.

Answer 2

Edward Kmett la réponse est évidemment très intéressant. Mais, c'est un peu technique. Ici est peut-être plus accessible explication.

Gratuit monades sont une façon de transformer les foncteurs dans les monades. C'est, étant donné un foncteur f Free f est une monade. Ce ne serait pas très utile, sauf que 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 de ces vous permet de "pénétrer dans" votre monade, et le second vous donne un moyen de "sortir" de celui-ci.

Plus généralement, si X est un Y avec quelques trucs supplémentaires P, puis un "libre-X" est un moyen d'obtenir de un Y pour un X sans en tirer grand chose de plus.

Exemples: un monoïde (X) est un ensemble (Y) avec structure supplémentaire (P) qui dit en gros il a un opérations (addition) et certains d'identité (comme zéro).

donc

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

maintenant, nous savons tous que les listes de

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

ainsi, compte tenu de tout type t nous savons qu' [t] est un monoïde

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

et si les listes sont les "monoïde libre" sur les ensembles (ou en Haskell types).

Ok, donc libre monades sont de la même idée. Nous prenons un foncteur, et donner une monade. En fait, depuis les monades peuvent être considérés comme monoids dans la catégorie de l'endo foncteurs, la définition d'une liste

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

ressemble beaucoup à la définition de la libre monades

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

et la Monade instance a une similitude avec le Monoïde exemple 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)

Answer 3

Un gratuit toto arrive à être la chose la plus simple qui satisfait à tous les 'foo' lois. C'est-à-dire qu'il remplit exactement les lois nécessaires pour être un " foo " et rien de plus.

Une oublieux foncteur est celui qui "oublie" une partie de la structure qu'il passe d'une catégorie à l'autre.

Compte tenu de foncteurs F : D -> C, et G : C -> D, nous disons F -| G, F est à gauche adjoint à l' Gou G est juste adjoint à l' F chaque fois que forall a, b: F a -> b est isomorphe a' a -> G b, là où les flèches viennent les catégories appropriées.

Formellement, un gratuit foncteur est à gauche adjoint à un oublieux foncteur.

Le Monoïde Libre

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

Prendre un monoïde, qui est définie par certaines transporteur établi T, une fonction binaire pour écraser une paire d'éléments d' f :: T → T → T, et un unit :: T, de sorte que vous avez une associatif loi, et une loi sur l'identité: f(unit,x) = x = f(x,unit).

Vous pouvez faire un foncteur U de la catégorie des monoids (où les flèches sont monoïde homomorphisms, c'est de s'assurer qu'ils carte unit de unit sur les autres monoïde, et que vous pouvez composer avant ou après la cartographie à l'autre monoïde sans changer la signification de la catégorie des jeux (d'où les flèches sont juste en fonction des flèches) qui "oublie" à propos du fonctionnement et de l' unit, et vous donne juste le transporteur établi.

Ensuite, vous pouvez définir un foncteur F de la catégorie des jeux de retour à la catégorie de monoids qui est à gauche adjoint de ce foncteur. Que le foncteur est le foncteur qui associe un ensemble a pour le monoïde [a]où unit = [], et mappend = (++).

Donc à revoir notre exemple, jusqu'à présent, dans la pseudo-Haskell:

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

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

Alors de montrer F est libre, à démontrer qu'elle est de gauche adjoint à l' U, oublieux foncteur, qui est, comme nous l'avons mentionné ci-dessus, nous avons besoin de montrer que

F a → b est isomorphe a' a → U b

maintenant, rappelez-vous la cible d' F est dans la catégorie Mon de monoids, où les flèches sont monoïde homomorphisms, donc nous avons besoin de montrer qu'un monoïde homomorphism de [a] → b peut être décrite précisément par une fonction à partir d' a → b.

En Haskell, nous appelons le côté de ce qui vit en Set (er, Hask, la catégorie de Haskell types que nous avons de faire semblant kit), foldMap, lorsque spécialisés de Data.Foldable pour les Listes de type Monoid m => (a → m) → [a] → m.

Il y a des conséquences que cela fait d'être un contiguïté. Notamment si vous oubliez puis construire avec gratuit, puis l'oublier à nouveau, juste comme vous l'avez oublié une fois, et nous pouvons l'utiliser pour construire la monadique rejoindre. depuis UFUF ~ U(FUF) ~ UF, et nous pouvons passer à l'identité monoïde homomorphism de [a] de [a] grâce à l'isomorphisme qui définit notre contiguïté,obtenir une liste isomorphisme de [a] → [a] est une fonction de type a -> [a], et c'est le juste retour pour les listes.

Vous pouvez composer tout cela plus directement par la description d'une liste en ces termes:

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

La Libre Monade

Alors, quel est un Gratuit Monade?

Eh bien, nous faisons la même chose que nous avons fait avant, nous commençons avec une oublieux foncteur U à partir de la catégorie des monades où les flèches sont monade homomorphisms à une catégorie de endofunctors où les flèches sont les transformations naturelles, et nous recherchons un foncteur qui est à gauche adjoint à que.

Alors, comment est-ce lié à la notion de libre monade comme il est généralement utilisé?

En sachant que quelque chose est gratuit monade, Free f, vous dit que le fait de donner une monade homomorphism de Free f -> m, c'est la même chose (isomorphe à) comme donnant une transformation naturelle (un foncteur homomorphism) à partir de f -> m. Rappelez-vous F a -> b doit être isomorphe a' a -> U b de F à gauche adjoint à U. U ici mappé monades de foncteurs.

F est au moins isomorphe à l' Free type que j'utilise dans mon free de package sur le hackage.

On pourrait aussi construire un resserrement analogie avec le code ci-dessus pour la liste libre, par définition

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 le droit adjoint à un oublieux foncteur en supposant qu'elle existe. Un cofree foncteur est tout simplement /droite adjoint/ pour une oublieux foncteur, et par symétrie, sachant que quelque chose est une cofree comonad est le même que de savoir que le fait de donner un comonad homomorphism de w -> Cofree f est la même chose que de donner à une transformation naturelle de w -> f.

Answer 4

La Libre Monade (structure de données) est à la Monade (classe) à l'instar de la Liste (structure de données) pour le Monoïde (classe): C'est la banalité de la mise en œuvre, où vous pouvez décider ensuite comment le contenu sera combiné.

---

Vous savez probablement ce qu'est une Monade est et que chaque Monade besoins spécifiques (Monade-respectueux de la loi) de la mise en œuvre de fmap + join + return ou bind + return.

Supposons que vous avez un Foncteur (une implémentation de l' fmap), mais le reste dépend des valeurs et des choix faits au moment de l'exécution, ce qui signifie que vous voulez être en mesure d'utiliser la Monade propriétés mais que vous voulez choisir la Monade-fonctions par la suite.

Qui peut être fait en utilisant la connexion Monade (structure de données), qui enveloppe le Foncteur (type) de telle manière que l' join est plutôt un empilement de ces foncteurs d'une réduction.

Le réel return et join vous souhaitez utiliser, peut à présent être donné en paramètres à la fonction de réduction de 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 f avec Monad m et b avec (m a):

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

Answer 5

Un Haskell gratuit monade 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))

Pure est analogue à l' Nil et Free est analogue à l' Cons. Un gratuit monade stocke une liste de foncteurs au lieu d'une liste de valeurs. Techniquement, vous pourriez en œuvre des monades à l'aide d'un type de données différent, mais toute la mise en œuvre doit être isomorphe à la ci-dessus.

Vous utilisez gratuit monades chaque fois que vous avez besoin d'un arbre de syntaxe abstraite. La base foncteur de la libre monade est la forme de chaque étape de l'arbre syntaxique.

Mon post, quelqu'un a déjà lié, donne plusieurs exemples de la façon de construire l'arbre de syntaxe abstraite avec gratuit monades