tag:blogger.com,1999:blog-1777990983847811806.post171760268230001678..comments2015-01-30T12:20:59.509-08:00Comments on Haskell for all: The category design patternGabriel Gonzaleznoreply@blogger.comBlogger20125tag:blogger.com,1999:blog-1777990983847811806.post-20602181034681638562012-10-27T07:44:16.240-07:002012-10-27T07:44:16.240-07:00You are correct. The a and b are the objects and ...You are correct. The a and b are the objects and they are Haskell types. So, interestingly, when you generalize pipes to proxies then you get two extra categories (see the Interact class in Control.Proxy.Class) and they do make use of the r parameter.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-82990345512469828912012-10-27T05:23:43.428-07:002012-10-27T05:23:43.428-07:00So, what *are* the objects for the Pipe category? ...So, what *are* the objects for the Pipe category? Are they Haskell types, just like in Hask? Are the objects on either side of the Pipe morphism represented by 'a' and 'b' in "Pipe a b r"? and if so, what does 'r' represent? If not, how far off the mark am I, exactly? :)Bryan Richterhttp://www.blogger.com/profile/00380593834900043397noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-78580732980534280482012-10-22T10:20:59.437-07:002012-10-22T10:20:59.437-07:00Thanks for the kind words! I've actually been...Thanks for the kind words! I've actually been learning from Awodey's book since I don't have a very strong mathematical background for MacLane's book, yet, but I plan to work through it eventually.<br /><br />I was plan on doing a follow-up post discussing objects (mainly in the context of Haskell types). Even in my own code with long composition chains, I often annotate the type of each intermediate step as a comment to help keep track of what is going on.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-79577427174884343682012-10-19T02:31:43.938-07:002012-10-19T02:31:43.938-07:00oops, speaking of noncommutativity, that's &qu...oops, speaking of noncommutativity, that's "Saunders MacLane", of course!stephen@xemacshttp://www.blogger.com/profile/02458669418391940756noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-90175223232161968222012-10-19T02:28:24.928-07:002012-10-19T02:28:24.928-07:00By the way, talking about "order of grouping&...By the way, talking about "order of grouping" is a little awkward (composition is generally not commutative). I think if you rephrase to something like "nesting of groups" the flow will be more natural for the reader.stephen@xemacshttp://www.blogger.com/profile/02458669418391940756noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-37706619069181349602012-10-19T02:25:21.481-07:002012-10-19T02:25:21.481-07:00You don't really need to apologize. Saying th...You don't really need to apologize. Saying the "category of X" where X is the objects is a trope. (Consider the usual description of a monoid as a category: how many monoids can be defined on a given set? All of them, and you don't even need any elements in the set as long as you don't ask that the arrows be functions!) OTOH, if you have the morphisms, then (via the source and target maps of the identities) you have the objects.<br /><br />As MacLane Saunders points out, it takes courage to name your categories by the common names of their arrows, rather than by the common names of their objects. I honor your bravery!<br /><br />Your point about "what the programmer works with" is well-taken, except that one reason why so many programmers don't get functional programming (at least at first) is because they want to work with objects. What you could say here is something like "the morphisms are what you work with if you want to achieve elegant, compact programs expressing complex relationships."stephen@xemacshttp://www.blogger.com/profile/02458669418391940756noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-16874072148768450092012-08-22T07:17:25.674-07:002012-08-22T07:17:25.674-07:00Thank you very much! I understand enough French t...Thank you very much! I understand enough French to know you did an excellent job of translation.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-66457705459858156412012-08-22T06:54:15.988-07:002012-08-22T06:54:15.988-07:00done at http://blog.demotera.com/published/2012-08...done at http://blog.demotera.com/published/2012-08-22-Programmation-Fonctionnelle-et-Theorie-des-Categories.htmlPaulhttp://www.blogger.com/profile/04809113583211386483noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-77647233203318368012012-08-21T07:04:17.601-07:002012-08-21T07:04:17.601-07:00That sounds great! I really appreciate it.That sounds great! I really appreciate it.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-14327434939571480002012-08-21T02:29:11.854-07:002012-08-21T02:29:11.854-07:00Hi Gabriel, nice post.
I was planning to write so...Hi Gabriel, nice post.<br /><br />I was planning to write something on the same topic, but in french, sometime in the near future. Haskell documentation is lacking in this dialect, and I hope that adding more content will create more opportunities for people to get into the purely functional way of programming.<br /><br />If you agree, I could also translate this good article, and credit it clearly of course. What do you think about that ?Paulhttp://www.blogger.com/profile/04809113583211386483noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-42378143318825945422012-08-19T12:43:44.625-07:002012-08-19T12:43:44.625-07:00Sorry, I made a mistake (read your reply too quick...Sorry, I made a mistake (read your reply too quickly), of course you can say 7 = id 7 because this is just 7 = 7.<br /><br />Well, at least from my way of thinking, you have two equalities:<br /><br />idP = Await (\a -> Yield a idP)<br /><br />and<br /><br />idP <+< idP = Await (\a -> Yield a (idP <+< idP))<br /><br />These are sort of "clearly" the same under a renaming. It may be true that you need deeper aspects of coinduction to prove it, but I'm not a good enough theorist to know :). sayntehttp://www.blogger.com/profile/09919237195037728981noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-57711118108619463412012-08-19T10:27:54.570-07:002012-08-19T10:27:54.570-07:00The correction is appreciated. If I didn't en...The correction is appreciated. If I didn't enjoy being corrected I wouldn't be programming in Haskell in the first place!<br /><br />I suppose there needs to be a better word for describing the "the category whose morphisms are X" because I agree that the way I phrased it bastardizes the terminology. From my perspective, what the programmer sees and works with are the morphisms, which is why I try to present categories in terms of the morphisms. Obviously the objects in the category affect which morphisms are compatible for composition, and I see that as being the second step of the presentation, not the first. I have to lead with the motivation (i.e. composition) otherwise it will read like every other category theory introduction which presents a bunch of rules and formalisms with no discussion of why we even need category theory in the first place.<br /><br />I tried to make it clear that each monad generates its own Kleisli category, but in retrospect I see that I described it the wrong way. I need to think about how to word it better so that the description still flows.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-21545360253324414312012-08-19T09:42:37.153-07:002012-08-19T09:42:37.153-07:00OK, let me see if I've got this straight.
From...OK, let me see if I've got this straight.<br />From the *definition*<br /><br /> foo = id foo<br /><br />I can conclude that foo is the *least* (well-defined) fixed point of id, i.e. bottom.<br /><br />From the mere (easy to prove) equality <br /><br /> 7 = id 7<br /><br />I can only conclude that 7 is *some* fixed point of id, not that 7 = foo.<br /><br />Similarly, from the definition<br /><br /> idP = Await (\a -> Yield a idP)<br /><br />I can conclude that idP is the least well-defined fixed point of the function G = \f -> Await (\a -> Yield a f),<br />whereas from the mere equality (not definition)<br /><br /> idP <+< idP = Await (\a -> Yield a (idP <+< idP))<br /><br />I can only conclude that idP <+< idP is *some* fixed point of G, not (without more) that idP <+< idP = idP.<br /><br />The missing piece might be that there is only one fixed point of G. That seems plausible to me, although right now I'm not sure how to prove it. It might be related to Gabriel's comment about bisimulation and coinduction.myzoskihttp://www.blogger.com/profile/02622704681931775367noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-79731452224777064552012-08-18T22:27:31.456-07:002012-08-18T22:27:31.456-07:00Well, remember that here you are *defining* (for e...Well, remember that here you are *defining* (for example):<br /><br />foo = id foo<br /><br />that's what foo *means*. You cannot say that 7 = id 7 because 7 *means* something else: it has another definition. The previous was fine because I was picking a fresh name (for example "f") that had no previous definition. <br /><br />The substitution was actually just to show you that your proof worked because your equality had the right 'structure', not because you already knew that "idP <+< idP = idP".<br /><br />I hope that helps!sayntehttp://www.blogger.com/profile/09919237195037728981noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-61457432807267764832012-08-18T21:42:54.492-07:002012-08-18T21:42:54.492-07:00I hate to be the snooty mathematician who corrects...I hate to be the snooty mathematician who corrects terminology, but here goes.<br /><br />When you say something is the "category of X" you really mean the objects in that category are X and you have to define the morphisms separately. For instance, your first category of Haskell functions is actually (probably) the category of Haskell types, and you defined the morphisms to be Haskell functions. If your category was really the category of Haskell functions, then your morphisms would need to be morphisms of Haskell functions.<br /><br />Of course, with the right tinkering you can blur the distinction between an object and the identity morphism on that object, but then the objects are still not *all* morphisms.<br /><br />Another thing to note is that the Kleisli category is defined per monad. So it's not the category of all monadic functions across all possible monads.<br /><br />I like the explanations though! I need to get back into Haskell myself.j2kunhttp://www.blogger.com/profile/08041921049916424212noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-70632842577106844382012-08-18T17:35:04.092-07:002012-08-18T17:35:04.092-07:00This comment has been removed by the author.myzoskihttp://www.blogger.com/profile/02622704681931775367noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-33341082602703549092012-08-18T17:23:03.572-07:002012-08-18T17:23:03.572-07:00Hi Saynte,
Thanks! I think you are right, but I wa...Hi Saynte,<br />Thanks! I think you are right, but I was wondering if I can always conclude from<br /><br /> f = G f<br />and g = G g<br /><br />that f = g. It's certainly not always true -- for instance<br />if I make the _definition_<br /><br />foo :: a<br />foo = id foo<br /><br />then I have defined foo to be bottom; but I can't conclude<br />from the fact that<br /><br />7 = id 7<br /><br />that 7 = foo.<br />myzoskihttp://www.blogger.com/profile/02622704681931775367noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-80419031254806708932012-08-18T15:19:36.644-07:002012-08-18T15:19:36.644-07:00You don't even have to assume what you want to...You don't even have to assume what you want to prove! You have the following:<br /><br />idP <+< idP = Await (\x -> Yield x (idP <+< idP))<br /><br />let f = idP <+< idP and do the substitution:<br /><br />f = Await (\x -> Yield x f)<br /><br />this is merely the definition of idP under a simple substitution. Voila, you have your proof.sayntehttp://www.blogger.com/profile/09919237195037728981noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-42289446959835481072012-08-18T10:17:52.584-07:002012-08-18T10:17:52.584-07:00I believe the correct term for this style of proof...I believe the correct term for this style of proof is bisimulation. Rather than use induction to show that the type is finite and use induction, you instead use coinduction to show that the generation of each subsequent constructor is finite and never bottoms. I believe the only example where composition fails to generate a constructor in a finite number of steps is:<br /><br />discard = Await $ \_ -> discard<br />supply = Yield () supply<br /><br />discard <+< supply<br /><br />... and that is precisely the only situation where pipe composition bottoms and fails to produce a result.<br /><br />However, I never intended this to be that complicated. It was merely an exercise so that users could practice equationally reasoning about laws. I assumed most of them would accept that the recursion in the proof was legitimate even if perhaps they could not precisely articulate the reason why.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-90028946580675334192012-08-18T09:45:24.279-07:002012-08-18T09:45:24.279-07:00" I leave it as an exercise for the reader to..." I leave it as an exercise for the reader to prove that they actually do form a category"<br /><br />OK, I'll bite. But let's try a special case of the identity laws, i.e. showing that idP <+< idP = idP:<br /><br />idP <+< idP<br />= Await (\a -> Yield a idP) <+< Await (\a' -> Yield a' idP)<br />= Await (\x -> idP <+< (\a' -> Yield a' idP) x)<br />= Await (\x -> idP <+< Yield x idP)<br />= Await (\x -> Await (\a -> Yield a idP) <+< Yield x idP)<br />= Await (\x -> (\a -> Yield a idP) x <+< idP)<br />= Await (\x -> Yield x idP <+< idP)<br />= Await (\x -> Yield x (idP <+< idP))<br /><br />Now, if I had (idP <+< idP) = idP on the inside, this would reduce to<br />= Await (\x -> Yield x idP)<br />= idP,<br /><br />but that would just be assuming what I want to prove.<br /><br />More generally, when I try to prove the category laws for Pipe a b r, I run into cases where if I could prove the law for a sub-expression, I could prove it for the whole expression, which makes me want to do induction; but presumably I also want to be able to prove results for circular, self-recursive pipes like idP in which there is no guarantee that the sub-expressions are 'smaller' than the original expression, so I don't know what to do.<br /><br />I figure this must have something to do with domain theory and least fixed points and supremums and all that, but I haven't worked all the way through that material so I'm not sure how the proof would look...myzoskihttp://www.blogger.com/profile/02622704681931775367noreply@blogger.com