Monads on all sides - Mathematical, diagonal and programmatic

I am trying to reconcile the categorical definition of the Monad with other general concepts / definitions that I have seen in some other textbooks / books.

Below, I can (perhaps decisively) try to close these two definitions, please point out errors and make corrections where ever required

So, starting with the definition of Monads

Monads are simply monoids in the category of endofuntors.

and with a little understanding of endofunctors, I guess Monad can be written as

((a->b)->Ma->Mb)->((b->c)->Mb->Mc) 

The " Type " is LHS (left side) Mb , and the RHS type is Mc , so I can write it below

 Mb-> (b->c)-> Mc, **which is how we define bind** 

And this is how I see Monads in the endofuctors category (which themselves are in Category C, with ' types ' as objects )

Monad visually .

Does that make sense?

+6
source share
3 answers

Well, I think you are a little gone. A monad is an endonuktor, which in Hask (a category of Haskell types) is something like the form F :: * -> * with some function that knows how to introduce morphisms (functions) into the Hask subcategory with functions on F as morphisms and F like objects, fmap . What you have seems to be a natural conversion to Hask.

Examples: Maybe , Either a , (,) a , etc.

Now the monad should also have 2 natural transformations ( Functor F, Functor g => F a -> G a in hask).

 n : Identity -> M u : M^2 -> M 

Or in haskell code

 n :: Identity a -> M a -- Identity a == a u :: M (M a) -> M a 

which correspond to return and join respectively.

Now we need to get to >>= . What you had as a binding was actually just fmap , we really want ma -> (a -> mb) -> mb . It is easy to determine how

  m >>= f = join $ f `fmap` m 

TA-dah! We have monads. Now for this monoid is endofentors.

A monoid over endofuntors would have functors as objects and natural transformations as morphisms. Interestingly, the product of two endofentors is their composition. Here is the Haskell code for our new monoid

 type (f <+> g) a = f (ga) class Functor m => Monoid' m where midentity' :: Identity a -> ma mappend' :: (m <+> m) a -> ma 

This desugar on

  midentity' :: a -> ma mappend' :: m (ma) -> ma 

Look familiar?

+9
source

The definition of "Monads is just monoids in the category of endofuntors", which, although true, is a bad place to start. This is from a message that was mainly intended as a joke. But if you are interested in correspondence, this can be demonstrated in Haskell:

Description of non-professionals categories is an abstract collection of objects and morphisms between objects. Comparisons between categories are called functors and map objects for objects and morphisms for morphisms associatively and identities are preserved. Entofuctor is a functor from the category into itself.

 {-# LANGUAGE MultiParamTypeClasses, ConstraintKinds, FlexibleInstances, FlexibleContexts #-} class Category c where id :: cxx (.) :: cyz -> cxy -> cxz class (Category c, Category d) => Functor cdt where fmap :: cab -> d (ta) (tb) type Endofunctor cf = Functor ccf 

Mappings between functors that satisfy the conditions of the identifier of the triangle and the identifier of associativity and are defined as:

  • η : 1 → T
  • μ : T^2 → T

In Haskell, μ is join and η is return

  • return :: Monad m => a -> ma
  • join :: Monad m => m (ma) -> ma

A categorical definition of Monad in Haskell can be written:

 class (Endofunctor ct) => Monad ct where eta :: ca (ta) mu :: c (t (ta)) (ta) 

The binding operator can be obtained from them.

 (>>=) :: (Monad ct) => ca (tb) -> c (ta) (tb) (>>=) f = mu . fmap f 

This is a complete definition, but, equivalently, you can also show that Monad laws can be expressed as monoid laws with a functor category. We can construct this category of functors, which is a category with objects as functors (i.e., Mappings between categories) and natural transformations (i.e., Mappings between functors) as morphisms. In the category of endofunctors, all functors are functors between the same category.

 newtype CatFunctor ctab = CatFunctor (c (ta) (tb)) 

We can show that this leads to a category with functor composition as a composition of morphism:

 -- Note needs UndecidableInstances to typecheck instance (Endofunctor ct) => Category (CatFunctor ct) where id = CatFunctor id (CatFunctor g) . (CatFunctor f) = CatFunctor (g . f) 

A monoid has the usual definition:

 class Monoid m where unit :: m mult :: m -> m -> m 

The monoid over the category of functors has natural transformations as the identity a and the multiplication operation, which combines the natural transformations. The composition of Claysley can be determined to satisfy the law of multiplication.

 (<=<) :: (Monad ct) => cy (tz) -> cx (ty) -> cx (tz) f <=< g = mu . fmap f . g 

And so you have it: "Monads are simply monoids in the category of endofentors", which is simply a "meaningless" version of the normal definition of monads from endofuntors and (mu, eta).

 instance (Monad ct) => Monoid (ca (ta)) where unit = eta mult = (<=<) 

With some substitution, it can be shown that monoidal properties (<=<) are equivalent statements of triangle diagrams and associativity for natural monad transformations.

 f <=< unit == f unit <=< f == f f <=< (g <=< h) == (f <=< g) <=< h 

If you are interested in diagrammatic representations, I wrote a little about representing them with string diagrams.

+5
source

It seems to me that you have omitted important things:

  • The definition has the word "monoid". You did not consider it in your post.
  • It is better to replace it with a "monoid object" to be exact. Monoids live in abstract algebra, monoid objects live in category theory. Different kinds.
    • Monoids are monoid objects in a certain category, but this is not relevant here.
  • A monoidal object can only be defined in the monoidal category.

So, the path to understanding the definition is as follows.

  • You are considering the endofunctors category (let's call it E ) in the Haskell Hask type and function category . Its objects are functors on Hask , the morphism in it from F to G is a polymorphic function of type F a → G a with some property.
  • You are considering a structure on E that turns it into a monoidal category, i.e. composition of functors and identical functors.
  • You are considering the definition of a monoid object, for example. from Wikipedia.
  • You think this means in your specific category E. This means that M is an endofunctor, and μ is of the same type as "join", and η is of the same type as "return".
  • "(→ =)" is defined through "join".

Tip. Do not try to express everything in Haskell. It is intended for writing programs, not for mathematics. Mathematical notation is more convenient here, because you can write the composition of functors as "∘" without going into the problem of type checking.

+2
source

Source: https://habr.com/ru/post/954303/


All Articles