tag:blogger.com,1999:blog-22587889.post6817569772136922840..comments2024-02-11T13:21:47.930+05:30Comments on Ruminations of a Programmer: List Algebras and the fixpoint combinator MuAnonymoushttp://www.blogger.com/profile/01613713587074301135noreply@blogger.comBlogger3125tag:blogger.com,1999:blog-22587889.post-37489719719587898962012-03-02T04:03:22.244+05:302012-03-02T04:03:22.244+05:30Debashish: Thought I'd done so earlier, but ju...Debashish: Thought I'd done so earlier, but just wanted to say "thanks" for the answer and reading recommendation. Best to you!Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-22587889.post-45697911949098365242012-01-31T11:21:55.442+05:302012-01-31T11:21:55.442+05:30Tim:
First I apologize if the post didn't mak...Tim:<br /><br />First I apologize if the post didn't make complete sense to you. At the same time I must admit that the content of the post may not make sense (a) at the first reading to the uninitiated and (b) if you don't care about the basic theory behind what you are implementing. It happened to me as well, when I first started digging deep into the subject.<br /><br />For me it all started when I took up TAPL (Types and Programming Languages) by Benjamin Pierce. If you are a regular reader of my blog, you must be aware that one of the things that I get interest in is *types*. I like typed programming, implementation of type systems particularly with respect to functional programming languages. And there's hardly a better introduction to that than TAPL.<br /><br />Assuming that you have interest in knowing some amount of type theory, one related subject that comes up together with it is category theory. You really can't learn type theory w/o a knowledge of category theory.<br /><br />But let's see why we need to understand fixpoints. All of us have written recursive functions. But how do you write an anonymous recursive function ? You need to know about fixpoints for this. Fixpoints can be defined for untyped lambda calculus as well as for typed lambda calculus. Fixpoints can be defined at the value level (Y) or at the type level (Mu). Mu is the fixpoint (or more precisely, the least fixpoint) for types and we need it to understand the concept of recursive types (e.g. List, Tree etc.). But why do we care about Mu ? We can use java.util.List day in and day out without even caring about what Mu gives. Sure we can. But again, we frequently hear that a recursive data type like a Tree is also known as *algebraic data type*. Why ? What's the *algebra* behind this data type ? If you seek answers to these questions, then you will be led to the world of categories, algebras and morphisms. <br /><br />As I showed through the last 2 posts on Mu, we can approach the subject from 2 sides - (a) type theory where we define it as a fixpoint and (b) from category theory where we show the algebra that defines Mu. The beauty of the 2 points of view is the unification through the definition of isomorphism between the two.<br /><br />I hope I have been able to shed some light towards the usefulness of these concepts. But again feel free to ignore at your discretion. You may not need all these at your day job. I also don't need them for the work which I do from 9 to 5.Anonymoushttps://www.blogger.com/profile/01613713587074301135noreply@blogger.comtag:blogger.com,1999:blog-22587889.post-18595940685553465752012-01-31T01:40:16.047+05:302012-01-31T01:40:16.047+05:30Debashish:
Sorry if this is a bit off-topic, and ...Debashish:<br /><br />Sorry if this is a bit off-topic, and sorry for appearing (or, more honestly, being) a bit clueless:<br /><br />I enjoy your blog -- even if I don't always understand it. I've been trying to get into FP a bit, to understand it more (thanks for the list of resources, BTW -- haven't started reading them yet, but hope to, soon) -- but the big question which keeps hitting over the head is: "Why?"<br /><br />In this case (reading back to what seems to be the seminal post in this series -- on bananas, lenses, and "fixpoints") -- is this just an interesting puzzle-solving exercise, or is there some kind of real-world applicability? Would you envision using Mu (for example) in an application -- or would you consider such an approach basically unmaintainable by ordinary programmers?<br /><br />(Forgive me: I expect, if I understood the subject more, I would know the answer to that -- but I find myself in a loop: having to put in lots of reading and effort to understand what people are saying, while not quite understanding *why* I should care -- which I expect I'm supposed to learn after I've deciphered the discussion.)<br /><br />FP is, I admit, a bit of mystery to me. Yes, I get the whole point of immutability, lack of side-effects, etc -- but my eyes often glaze over when I see what seems to be a simple concept (say, EIP's word counter) implemented in a manner which, I'm pretty sure almost no-one I work with (or have ever worked with) would understand. I puzzle at the ongoing fascination with monads, and people doing (seemingly) hours of work rewriting an API to add a "print" statement to it -- or achieve some other mundane effect.<br /><br />While I admire such mental prowess, I'm still scratching my head trying to understand the attraction -- and since you actually seem to do real-life work, and seem fairly practical -- I thought I'd just blurt out the question and get your take on it. <br /><br />Regardless, thanks in advance. - TimAnonymousnoreply@blogger.com