<\/p>\n
Fundamentally, in category theory a monad is a category with a particular kind of structure. It’s a category with one<\/em> object. That category has a collection of arrows which (obviously) are from the single object to itself<\/em>. That one-object category has a functor<\/em> from the category to itself. (As a reminder, a functoris an arrow between categories in the category of (small) categories.) <\/p>\n The first trick to the monad, in terms of theory, is that it’s fundamentally<\/em> about the functor: since the functor maps from a category to the same category<\/em>, so you can almost ignore the category; it’s implicit in the definition of the functor. So we can almost treat the monad as if it were just the functor – that is, a kind of transition function.<\/p>\n The other big trick is closely related to that. For the programming language application of monads, we can think of the single object in the category as the set of all possible states. So we have a category object, which is essentially the collection of all possible states; and there are arrows between the states representing possible state transitions. So the monad’s functor is really just a mapping from arrows to different arrows – which basically represents the way that changing the state causes a change in the possible transitions to other states. <\/p>\n So what a monad gives us, in terms of category theory, in a conceptual framework that captures the concept of a state transition system, in terms of transition functions that invisibly<\/em> carry a state. When that’s translated into programming languages, that becomes a value<\/em> that implicitly takes an input state, possibly updates it, and returns an output state. Sound familiar? <\/p>\n Let’s take a moment and get formal. As usual for category theory, first there are some preliminary definitions.<\/p>\n Now, with that out of the way, we can give the complete formal definition of a monad. Given a category C<\/b>, a monad on C<\/b><\/em> is a triple: (T<\/b>:C<\/b>→C<\/b>, η:1C<\/sub>→T<\/b>, μ:T<\/b>2<\/sup> → T<\/b>), where T<\/b> is a functor, and η and μ are natural transformations. The members of the triple must make the following two diagrams commute.<\/p>\n <\/p>\n Commutativity of composition with μ<\/em><\/p>\n <\/p>\n Commutativity of composition with η<\/em><\/p>\n What these two diagrams mean is that successive applications of the state-transition functor over C<\/b> behave associatively – that any sequence of composing monadic functors will result in a functor with full monadic structure; and that the monadic structure will always preserve. Together, these mean that any sequence of operations (that is, applications of the monad functor) are themselves monad functors – so the building a sequence of monadic state transformers is guaranteed to behave as a proper monadic state transition – so what happens inside<\/em> of the monadic functor is fine – to the rest of the universe, the difference between a sequence and a single simple operation is indistinguishable: the state will be consistently passed from application to application with the correct chaining behavior, and to the outside world, the entire monadic chain looks like like a single atomic monadic operation.<\/p>\n Now, what does this mean in terms of programming? Each element of a monadic sequence in Haskell is an instantiation of the monadic functor – that is, it’s an arrow<\/em> between states – a function, not a simple value – which is the basic trick to monads. They look like a sequence of statements<\/em>; in fact, each statement in a monad is actually a function from state to state. And it looks like we’re writing sequence code – when what we’re actually doing is writing function compositions<\/em> – so that when we’re done writing a monadic sequence, what we’ve actually<\/em> done is written a function definition<\/em> in terms of a sequence of function compositions.<\/p>\n Understanding that, we can now clearly understand why we need the return<\/em> function to use a non-monad expression inside of a monadic sequence – because each step in the sequence needs to be an instance of the monadic functor; an expression that isn’t<\/em> an instance of the monadic functor couldn’t be composed with the functions in the sequence. The return function is really nothing but a function that combines a non-monadic expression with the id<\/em> functor. <\/p>\n In light of this, let’s go back and look at the definition of The declaration of monad is connected with the definition of functor – if you look, you can see the connection. The fundamental operation of So the value type wrapped in the monad is a functor – in fact, the<\/em> functor from the category definition! And the “ A proper implementation of a monad needs to follow some fundamental rules – the rules are, basically, just Haskell translations of the structure-preserving rules about functors and natural transformations in the category-theoretic monad. There are two groups of laws – laws about the There are two simple laws for The monad laws are a bit harder, but not much. The mainly govern how monadic operations interact with non-monadic operations in terms of the “ As promised, I’m finally going to get to the theory behind monads. As a quick review, the basic idea of the monad in Haskell is a hidden transition function – a monad is, basically, a state transition function. The theory of monads comes from category theory. I’m going to assume you know a little bit […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[76,89],"tags":[],"class_list":["post-294","post","type-post","status-publish","format-standard","hentry","category-category-theory","category-haskell"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-4K","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/294","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=294"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/294\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=294"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=294"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=294"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}\n
![\"monad-prop1.jpg\"](\"https:\/\/i0.wp.com\/scientopia.org\/img-archive\/goodmath\/img_300.jpg?resize=157%2C117\")
<\/p>\n
\n![\"monad-prop2.jpg\"](\"https:\/\/i0.wp.com\/scientopia.org\/img-archive\/goodmath\/img_301.jpg?resize=236%2C170\")
<\/p>\nMonad<\/code> in the Haskell standard prelude.<\/p>\n\nclass Functor f where\n fmap :: (a -> b) -> f a -> f b\n\nclass Monad m where\n (>>=) :: m a -> (a -> m b) -> m b\n (>>) :: m a -> m b -> m b\n return :: a -> m a\n fail :: String -> m a\n\n -- Minimal complete definition:\n -- (>>=), return\n m >> k = m >>= _ -> k\n fail s = error s\n<\/pre>\n
Monad<\/code> is “>>=<\/code>” – the chaining operation, which is type m a -> (a -> m b) -> m b<\/code> is deeply connected with the fmap<\/code> operation from Functor<\/code>‘s fmap<\/code> operation – the a<\/code> in m a<\/code> is generally going to be a type which can be a Functor<\/code>. <\/p>\n>>=<\/code>” operation is just the functor composition operation from the monad definition.<\/p>\nFunctor<\/code> class, which should hold for the transition function wrapped in the monad class; and laws about the monadic operations in the Monad<\/code> class. One important thing to realize about the functor and monad laws is that they are not enforced<\/em> – in fact, cannot<\/em> be enforced! – but monad-based code using monad implementations that do not follow them may not work correctly. (A compile-time method for correctly verifying the enforcement of these rules can be shown to be equivalent to the halting problem.)<\/p>\nFunctor<\/code>, and it’s pretty obvious why they’re fundamentally just strucure-preservation requirements. The functor class only has one operation, called fmap<\/code>, and the two functor laws are about how it must behave.<\/p>\n\n
fmap id = id<\/code>
(Mapping ID over any structured sequence results in an unmodified sequence)<\/em><\/li>\nfmap (f . g) = (fmap f) . (fmap g)<\/code>
(“.” is the function composition operation; this just says that fmap preserves the structure to ensure that that mapping is associative with composition.)<\/em><\/li>\n<\/ol>\nreturn<\/code>” and “>>=<\/code>” operations of the Monad<\/code> class.<\/p>\n\n
return x >>= f = f x<\/code>
(injecting a value into the monad is basically the same as passing it as a parameter down the chain – return is really just the identity functor passing its result on to the next step.)<\/em><\/li>\n f >>= return = f<\/code>
(If you don’t specify a value for a return, it’s the same as just returning the result of the previous step in the sequence – again, return is just identity, so passing something into return shouldn’t affect it.)<\/em><\/li>\nseq >>= return . f = fmap f seq<\/code>
(composing return with a function is equivalent to invoking that function on the result of the monad sequence to that point, and wrapping the result in the monad – in other words, it’s just composition with identity.)<\/em><\/li>\nseq >>= (x -> f x >>= g) = (seq >>= f) >>= g<\/code>
(Your implementation of “>>=<\/code>” needs to be semantically equivalent to the usual translation; that is, it must behave like a functor composition.)<\/em><\/li>\n<\/ol>\n","protected":false},"excerpt":{"rendered":"