{"id":1770,"date":"2012-05-13T20:36:13","date_gmt":"2012-05-14T00:36:13","guid":{"rendered":"http:\/\/scientopia.org\/blogs\/goodmath\/?p=1770"},"modified":"2020-08-04T09:15:35","modified_gmt":"2020-08-04T13:15:35","slug":"introducing-algebraic-data-structures-via-category-theory-monoids","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2012\/05\/13\/introducing-algebraic-data-structures-via-category-theory-monoids\/","title":{"rendered":"Introducing Algebraic Data Structures via Category Theory: Monoids"},"content":{"rendered":"

Since joining foursquare, I’ve been spending almost all of my time writing functional programs. At foursquare, we do all of our server programming in Scala, and we have a very strong bias towards writing our scala code very functionally.<\/p>\n

This has increased my interest in category theory in an interesting way. As a programming language geek, I’m obviously fascinated by data structures. Category theory provides a really interesting handle on a way of looking at a kind of generic data structures.<\/p>\n

Historically (as much as that word can be used for anything in computer science), we’ve thought about data structures primarily in a algorithmic and structural ways.<\/p>\n

For example, binary trees. A binary tree consists of a collection of linked nodes. We can define the structure recursively really easily: a binary tree is a node, which contains pointers to at most two other binary trees.<\/p>\n

In the functional programming world, people have started to think about things in algebraic ways. So instead of just defining data structures in terms of structure, we also think about them in very algebraic ways. That is, we think about structures in terms of how they behave<\/em>, instead of how they’re built<\/em>.<\/p>\n

For example, there’s a structure called a monoid. A monoid is a very simple idea: it’s an algebraic structure with a set of values S, one binary operation *, and one value i in S which is an identity value for *. To be a monoid, these objects must satisfy some rules called the monad laws<\/em>:<\/p>\n

    \n
  1. \\forall s \\in S: s * i = s, i * s = s<\/li>\n
  2. \\forall x, y, z \\in S: (x * y) * z = x * (y * z)<\/li>\n<\/ol>\n

    There are some really obvious examples of monoids – like the set of integers with addition and 0 or integers with multiplication and 1. But there are many, many others.<\/p>\n

    Lists with concatenation and the empty list are a monoid: for any list,
    \nl ++ [] == l, [] + l == l, and concatenation is associative.<\/p>\n

    Why should we care if data structures like are monoids? Because we can write very general code in terms of the algebraic construction, and then use it over all of the different operations. Monoids provide the tools you need to build fold<\/em> operations. Every kind of fold – that is, operations that collapse a sequence of other operations into a single value – can be defined in terms of monoids. So you can write a fold operation that works on lists, strings, numbers, optional values, maps, and god-only-knows what else. Any data structure which is a monoid is a data structure with a meaningful fold operation: monoids encapsulate the requirements of foldability.<\/p>\n

    And that’s where category theory comes in. Category theory provides a generic method for talking about algebraic structures<\/em> like monoids. After all, what category theory does is provide a way of describing structures in terms of how their operations can be composed: that’s exactly<\/em> what you want for talking about algebraic data structures.<\/p>\n

    The categorical construction of a monoid is, alas, pretty complicated. It’s a simple idea – but defining it solely in terms of the composition behavior of function-like objects does take a bit of effort. But it’s really worth it: when you see a monoidal category, it’s obvious what the elements are in terms of programming. And when we get to even more complicated structures, like monads, pullbacks, etc., the advantage will be even clearer.<\/p>\n

    A monoidal category is a category with a functor, where the functor has the basic properties of a algebraic monoid. So it’s a category C, paired with a bi-functor – that is a two-argument functor \u2297:C\u00d7C\u2192C. This is the categorical form of the tensor<\/em> operation from the algebraic monoid. To make it a monoidal category, we need to take the tensor operation, and define the properties that it needs to have. They’re called its coherence conditions<\/em>, and basically, they’re the properties that are needed to make the diagrams that we’re going to use commute.<\/p>\n

    So – the tensor functor is a bifunctor from C\u00d7C to C. There is also an object I\u2208C, which is called the unit object, which is basically the identity element of the monoid. As we would expect from the algebraic definition, the tensor functor has two basic properties: associativity, and identity.<\/p>\n

    Associativity is expressed categorically using a natural isomorphism, which we’ll name \u03b1. For any three object X, Y, and Z, \u03b1 includes a component \u03b1X,Y,Z<\/sub> (which I’ll label \u03b1(X,Y,Z) in diagrams, because subscripts in diagrams are a pain!), which is a mapping from (X\u2297Y)\u2297Z to X\u2297(Y\u2297Z). The natural isomorphism says, in categorical terms, that the the two objects on either side of its mappings are equivalent.<\/p>\n

    The identity property is again expressed via natural isomorphism. The category must include an object I (called the unit<\/em>), and two natural isomorphisms, called &lamba; and \u03c1. For any arrow X in C, &lamba; and \u03c1 contain components \u03bbX<\/sub> and \u03c1X<\/sub> such that \u03bbX<\/sub> maps from I\u2297X\u2192X, and \u03c1X<\/sub> maps from X\u2297I to X.<\/p>\n

    Now, all of the pieces that we need are on the table. All we need to do is explain how they all fit together – what kinds of properties these pieces need to have for this to – that is, for these definitions to give us a structure that looks like the algebraic notion of monoidal structures, but built in category theory. The properties are, more or less, exact correspondences with the associativity and identity requirements of the algebraic monoid. But with category theory, we can say it visually. The two diagrams below each describe one of the two properties.<\/p>\n

    \"monoidal-categoy.png\"<\/p>\n

    The upper (pentagonal) diagram must commute for all A, B, C, and D. It describes the associativity property. Each arrow in the diagram is a component of the natural isomorphism over the category, and the diagram describes what it means for the natural isomorphism to define associativity.<\/p>\n

    Similarly, the bottom diagram defines identity. The arrows are all components of natural isomorphisms, and they describe the properties that the natural isomorphisms must have in order for them, together with the unit I to define identity.<\/p>\n

    Like I said, the definition is a lot more complicated. But look at the diagram: you can see folding in it, in the chains of arrows in the commutative diagram.<\/p>\n","protected":false},"excerpt":{"rendered":"

    Since joining foursquare, I’ve been spending almost all of my time writing functional programs. At foursquare, we do all of our server programming in Scala, and we have a very strong bias towards writing our scala code very functionally. This has increased my interest in category theory in an interesting way. As a programming language […]<\/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,83,54],"tags":[],"class_list":["post-1770","post","type-post","status-publish","format-standard","hentry","category-category-theory","category-data-structures","category-programming"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-sy","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/1770","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=1770"}],"version-history":[{"count":1,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/1770\/revisions"}],"predecessor-version":[{"id":3866,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/1770\/revisions\/3866"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=1770"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=1770"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=1770"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}