La théorie de la monade et Haskell

Question

La plupart des tutoriels semblent donner beaucoup d'exemples de monades (IO, l'état, la liste et ainsi de suite) et puis attendre le lecteur à être en mesure de résumé le principe, et puis la mention de la catégorie de la théorie. Je n'ai pas tendance à très bien apprendre en essayant de généraliser à partir d'exemples et je voudrais comprendre, d'un point de vue théorique, pourquoi ce modèle est tellement important.

À en juger par ce fil: Quelqu'un peut-il expliquer les Monades? c'est un problème commun, et j'ai essayé de regarder la plupart des tutoriels suggéré (à l'exception de l'Brian Beck vidéos qui ne jouera pas sur ma machine linux):

Personne ne sait d'un tutoriel qui commence à partir de la catégorie de la théorie et de explique IO, l'état, la liste des monades dans ces conditions? ce qui suit est ma tentative infructueuse de le faire:

Je comprends qu'une monade se compose d'un triple: une endo-foncteur et deux transformations naturelles.

Le foncteur est généralement indiqué avec le type: (a -> b) -> (m a -> m b) J'ai inclus la deuxième support juste pour souligner la symétrie.

Mais, c'est un endofunctor, et donc ne devrait pas le domaine et l'arrivée être le même comme ceci?:

(a -> b) -> (a -> b)

Je pense que la réponse est que le domaine et l'arrivée ont tous les deux un type de:

(a -> b) | (m a -> m b) | (m -> m m b) et ainsi de suite ...

Mais je ne suis pas vraiment sûr si cela fonctionne ou s'inscrit dans la définition du foncteur donné?

Lorsque nous passons à la transformation naturelle c'est encore pire. Si je comprends bien une transformation naturelle est un second ordre foncteur (avec certaines règles) qui est un foncteur d'un foncteur à un autre. Alors, puisque nous avons défini le foncteur ci-dessus le type général de la les transformations naturelles serait: ((a -> b) -> (m a -> m b)) - > (a -> b) -> (m a -> m b))

Mais les transformations naturelles que nous utilisons sont de type:

a -> m a

m a -> (a ->m b) -> m b

Sont ces sous-ensembles de la forme générale ci-dessus? et pourquoi sont-ils les transformations naturelles?

Martin

Answer 1

Un rapide disclaimer: je suis un peu rouillée sur la catégorie de la théorie en général, alors que j'ai l'impression que vous avez au moins une certaine familiarité avec elle. J'espère que je ne vais pas en faire trop d'un hachage de ce...

Personne ne sait d'un tutoriel qui commence à partir de la catégorie de la théorie et de explique IO, l'état, la liste des monades dans ces conditions?

Tout d'abord, ignorer IO pour l'instant, c'est plein de magie noire. Il fonctionne comme un modèle de l'impératif de calculs pour les mêmes raisons qu' State travaux pour la modélisation de la dynamique des calculs, mais contrairement à cette dernière IO est une boîte noire avec aucun moyen de déduire le monadique de la structure de l'extérieur.

Le foncteur est généralement indiqué avec le type: (a -> b) -> (m a -> m b) j'ai compris la deuxième support juste pour souligner la symétrie.

Mais, c'est un endofunctor, et donc ne devrait pas le domaine et l'arrivée être le même comme ceci?:

Je soupçonne que vous êtes une mauvaise interprétation de la façon dont les variables de type en Haskell se rapportent à la catégorie de la théorie des concepts.

Tout d'abord, oui, qui spécifie un endofunctor, sur la catégorie de Haskell types. Une variable de type comme a n'est pas rien dans cette catégorie, cependant, c'est une variable qui est (implicitement) universellement quantifiée sur tous les objets de la catégorie. Ainsi, le type (a -> b) -> (a -> b) ne décrit que endofunctors que la carte chaque objet pour lui-même.

Type de constructeurs de décrire une fonction injective sur des objets, où les éléments du constructeur de l'arrivée ne peut pas être décrite par tous les moyens, sauf que l'application d'un constructeur de type. Même si les deux types de constructeurs de produire des isomorphe résultats, les types qui en résultent restent distinctes. À noter que la nature les constructeurs ne sont pas, dans le cas général, les foncteurs.

Le type de la variable m dans le foncteur signature, puis, représente un type d'argument du constructeur. Hors contexte, ce serait normalement être lu comme une quantification universelle, mais c'est incorrect dans ce cas, puisqu'une telle fonction ne peut pas exister. Plutôt, le type de définition de la classe de lie m et permet la définition de ces fonctions pour spécifique type des constructeurs.

La fonction obtenue, puis, indique que, pour tout type constructeur m qui a fmap défini, pour les deux objets quelconques a et b et un morphism entre eux, on peut trouver un morphism entre les types de données par application d' m de a et b.

Notez que tout ce qui précède n'est, bien sûr, de définir un endofunctor sur Hask, il n'est pas même à distance suffisamment général pour décrire tous ces endofunctors.

Mais les transformations naturelles que nous utilisons sont de type:

a -> m a

m a -> (a ->m b) -> m b

Sont ces sous-ensembles de la forme générale ci-dessus? et pourquoi sont-ils les transformations naturelles?

Eh bien, non, ils ne le sont pas. Une transformation naturelle est d'environ une fonction (pas un foncteur) entre foncteurs. Les deux les transformations naturelles qui spécifient une monade M ressembler I -> M où I est l'identité foncteur, et M ∘ M -> M où ∘ est foncteur de la composition. En Haskell, nous n'avons pas de bonne façon de travailler directement avec une vraie identité foncteur ou avec foncteur de la composition. Au lieu de cela, nous rejetons l'identité foncteur d' (Functor m) => a -> m a pour la première, et d'écrire imbriquée constructeur de type application en tant que (Functor m) => m (m a) -> m a pour la seconde.

La première est évidemment return; la deuxième est une fonction appelée join, ce qui n'est pas partie de la classe type. Toutefois, join peut être écrite en termes de (>>=), et le dernier est le plus souvent utile dans la journée-à-jour de programmation.

---

En tant que mesure spécifique monades aller, si vous voulez une description mathématique, voici un croquis rapide d'un exemple:

Pour certains type fixe S, considérons deux foncteurs F et G, où F(x) = (S, x) et G(x) = S -> x (Il devrait être évident que ceux-ci sont en effet valables foncteurs).

Ces foncteurs sont également adjoints; envisager les transformations naturelles unit :: x -> G (F x) et counit :: F (G x) -> x. L'expansion de l'définitions nous donne unit :: x -> (S -> (S, x)) et counit :: (S, S -> x) -> x. Les types suggèrent uncurried fonction de l'application et de tuple de la construction; n'hésitez pas à vérifier qu'ils fonctionnent comme prévu.

Une contiguïté donne lieu à une monade par la composition des foncteurs, donc, en prenant G ∘ F et l'élargissement de la définition, on obtient G (F x) = S -> (S, x), ce qui est la définition de l' State monade. L' unit de la contiguïté est évidemment return; et vous devriez être en mesure d'utiliser counit pour définir join.

Answer 2

Cette page fait exactement cela. Je pense que votre principale confusion est que la classe ne fait pas du type un foncteur, mais définit un foncteur de la catégorie des types Haskell dans la catégorie de ce type.

Suivant la notation du lien, en supposant que F est un foncteur de Haskell, cela signifie qu’il existe un foncteur de la catégorie de Hask à la catégorie de F.

Answer 3

Grosso modo, Haskell ne sa catégorie théorie dans une seule catégorie dont les objets sont Haskell types et dont les flèches sont des fonctions entre ces types. Ce n'est certainement pas un usage général de la langue pour la modélisation de la catégorie de la théorie.

Un (mathématiques) foncteur est une opération de tourner les choses dans une catégorie dans des choses d'une autre, éventuellement totalement différent, de la catégorie. Un endofunctor est alors un foncteur qui arrive à avoir la même source et cible les catégories. En Haskell, un foncteur est une opération de tourner les choses dans la catégorie des Haskell types dans d'autres choses aussi dans la catégorie de Haskell types, de sorte qu'il est toujours un endofunctor.

[Si vous êtes à la suite de la littérature mathématique, techniquement, l'opération "(a->b)->(m a -> m b) "n'est que la flèche de la partie de la endofunctor m, et" m " est la partie de l'objet]

Lorsque Haskellers parler de travailler dans une "monade", ils signifient vraiment de travail dans la catégorie de Kleisli de la monade. La catégorie de Kleisli une monade est un fond de confusion bête au premier abord, et normalement besoin d'au moins deux couleurs d'encre pour donner une bonne explication, afin de prendre la tentative suivante pour ce qu'il est et découvrez quelques références (malheureusement, Wikipédia est inutile ici pour tous, mais le droit définitions).

Supposons que vous avez une monade " m " sur la catégorie C de la Haskell types. Sa catégorie de Kleisli Kl(m) a les mêmes objets que C, à savoir Haskell types, mais une flèche un ~(f)~> b dans Kl(m) est une flèche de a -(f)-> mo C. (j'ai utilisé une ligne sinueuse dans mon Kleisli flèche pour distinguer les deux). Je le répète: les objets et les flèches de la Kl(C) sont aussi des objets et des flèches de C, mais les flèches pointent vers différents objets de Kl(C) que dans C. Si ce n'est pas vous frapper aussi étrange, le relire plus attentivement!

Concrètement, Peut-être envisager la monade. Sa catégorie de Kleisli est juste la collection de Haskell types, et ses flèches un ~(f)~> b sont des fonctions de a -(f)-> Peut-être que b. Ou de considérer l' (État s) monade dont les flèches sont un ~(f)~> b sont des fonctions de a -(f)-> (État s b) == a(f)-> (s->(s,b)). Dans tous les cas, vous êtes toujours à écrire un enchevêtrées flèche, comme un raccourci pour faire quelque chose pour le type de l'arrivée de vos fonctions.

[Notez que l'État n'est pas une monade, parce que l'État est * -> * -> *, de sorte que vous devez fournir l'un des paramètres de type de la transformer en mathématiques monade.]

C'est très bien, je l'espère, mais supposons que vous souhaitez composer des flèches un ~(f)~> b et b ~(g)~> c. Ce sont vraiment des Haskell fonctions a -(f)-> mo et b -(g)-> mc que vous ne pouvez pas composer parce que les types ne correspondent pas. La solution mathématique est d'utiliser la "multiplication" transformation naturelle u:mm->m de la monade comme suit: a ~f)~> b ~(g)~> c == a -(f)-> mo -(mg)-> mmc(u_c)-> mc pour obtenir une flèche a->mc qui est un Kleisli flèche d'un ~(f;g)~> c tel que requis.

Peut-être un exemple concret permet ici. Dans la monade Peut-être, vous ne pouvez pas composer des fonctions f : a -> Peut-être b et g : b -> Peut-être que c directement, mais en soulevant g de

Maybe_g :: Maybe b -> Maybe (Maybe c)
Maybe_g Nothing = Nothing
Maybe_g (Just a) = Just (g a)

et à l'aide de la "évidentes"

u :: Maybe (Maybe c) -> Maybe c
u Nothing = Nothing
u (Just Nothing) = Nothing
u (Just (Just c)) = Just c

vous pouvez former la composition u . Maybe_g . f ce qui est la fonction a -> Peut-être que c que tu voulais.

Dans l' (État s) monade, c'est similaire, mais messier: étant Donnés deux monadique des fonctions d'une ~(f)~> b et b ~(g)~> c qui sont vraiment un -(f)-> (s->(s,b)) et b -(g)-> (s->(s,c)) sous le capot, vous les composer en soulevant g en

State_s_g :: (s->(s,b)) -> (s->(s,(s->(s,c))))
State_s_g p s1 = let (s2, b) = p s1 in (s2, g b)

ensuite, vous appliquez la "multiplication" la transformation naturelle de u, qui est

u :: (s->(s,(s->(s,c)))) -> (s->(s,c))
u p1 s1 = let (s2, p2) = p1 s1 in p2 s2

qui (un peu) les bougies de l'état final de l' f dans l'état initial de l' g.

En Haskell, cela s'avère être un peu de façon naturelle à travailler si au lieu de cela, il y a la (>>=) fonction qui fait la même chose que u, mais d'une manière qui rend plus facile à implémenter et à utiliser. Ceci est important: (>>=) n'est pas la transformation naturelle de 'u'. Vous pouvez définir chacun des termes de l'autre, de sorte qu'ils sont équivalents, mais ils ne sont pas la même chose. Le Haskell version de " u " est écrit join.

L'autre chose qui manque à cette définition de Kleisli catégories est l'identité sur chaque objet: a ~(1_a)~> un qui est vraiment un -(n_a)-> ma, où n est le 'unité de transformation naturelle. C'est écrit return en Haskell, et ne semble pas causer beaucoup de confusion.

J'ai appris catégorie de théorie avant que j'arrive à Haskell, et j'ai aussi eu de la difficulté avec le décalage entre ce que les mathématiciens appellent une monade et à quoi ils ressemblent en Haskell. C'est pas plus facile dans l'autre sens!

Answer 4

Pas sûr de comprendre quelle était la question, mais oui, vous avez raison, la monade en Haskell est définie comme une triple:

m :: * -> * -- that is endofunctor from haskell types to haskell types!
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b

mais la définition commune de la catégorie de la théorie est un autre triple:

m :: * -> *
return :: a -> m a
join ::  m (m a) -> m a

Il est un peu confus, mais il n'est pas difficile de montrer que ces deux définitions sont équivalentes. Pour cela nous avons besoin de définir rejoindre en termes de (>>=) (et vice versa). Première étape:

join :: m (m a) -> m a
join x = ?

Cela nous donne de l' x :: m (m a).
Tout ce que nous pouvons faire avec quelque chose qui ont type m _ est à appliquer (>>=) pour elle:

(x >>=) :: (m a -> m b) -> m b

Maintenant, nous avons besoin de quelque chose comme un deuxième argument pour (>>=), et aussi, à partir du type de jointure nous avons contrainte (x >>= y) :: ma.
Donc y a de type y :: ma -> ma et id :: a -> a s'adapte très bien ici:

join x = x >>= id

L'autre façon

(>>=) :: ma -> (a -> mb) -> m b
(>>=) x y = ?

Où x :: m a et y :: a -> m b. Pour obtenir de l' m b de x et y nous avons besoin de quelque chose de type a.
Malheureusement, nous ne pouvons pas extraire a de m a. Mais on peut le remplacer par autre chose (rappelez-vous, monade est un foncteur aussi):

fmap :: (a -> b) -> m a -> m b
fmap y x :: m (m b)

Et il est parfaitement adapté comme argument pour join: (>>=) x y = join (fmap y x).

Answer 5

La meilleure façon de regarder les monades et de calcul des effets est de commencer par où Haskell a eu l'idée de monades pour le calcul des effets de partir, et puis regarder Haskell après vous comprenez que. Voir ce document en particulier: les Notions de Calcul et de Monades, par E. Moggi.

Voir aussi Moggi est un document antérieur, qui montre comment les monades de travail pour le lambda calcul seul: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.2787

Le fait que les monades de capture de substitution, entre autres choses (http://blog.sigfpe.com/2009/12/where-do-monads-come-from.html), et de la substitution est la clé pour le lambda calcul, devrait donner une bonne idée de pourquoi ils ont tellement de puissance expressive.