tag:blogger.com,1999:blog-1777990983847811806.post3458556845715291786..comments2014-04-20T20:07:14.535-07:00Comments on Haskell for all: Comonads are objectsGabriel Gonzaleznoreply@blogger.comBlogger20125tag:blogger.com,1999:blog-1777990983847811806.post-74509041673494009412013-03-14T11:35:22.244-07:002013-03-14T11:35:22.244-07:00Sorry for the really late response. You were righ...Sorry for the really late response. You were right and I fixed it. Thanks for pointing that out. That's a pretty important thing to get right. :)Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-54401209643481312342013-03-02T20:30:33.191-08:002013-03-02T20:30:33.191-08:00Wow! Thanks for the explanation.
My understandin...Wow! Thanks for the explanation.<br /><br />My understanding of what you said is that "necessarily" (i.e. the [] operator) reflects a property that must be true of all reachable worlds, not just the current one. So I think your []I rule says something like:<br /><br />"If we can infer 'A' even from an empty current world, that means that its truth must be independent of the selected world".<br /><br />Or, in other words, the [] reflects some sort of truth that *must* originate from a world-independent source.<br /><br />Then that would make sense as a comonad, since it's obviously true that if is something is true in a world-independent way, then it's still true in a world-dependent way:<br /><br />[]A -> A<br /><br />Similarly, if 'A' is true in a world independent way, then the "fact that it is true in a world-independent way" is itself true in a world-independent way:<br /><br />[]A -> [][]A<br /><br />In other words, world-independence is itself a world-independent property.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-73012456523258324912013-03-02T19:03:23.073-08:002013-03-02T19:03:23.073-08:00On "Pfenning-Davies" - since I'm Dav...On "Pfenning-Davies" - since I'm Davies: it's actually modal IS4 we focus on rather than IS5 (which wouldn't have such nice computational properties). <br /><br />Also the []I rule should be:<br /><br />\Delta ; \empty |- A<br />---------------------------[]I<br />\Delta ; \Gamma |- []A<br /><br />Here the semicolons separate two different contexts. The first context contains assumptions about validity, which hold in all reachable worlds. The second context holds assumptions about truth, which apply only for the current world.<br /><br />So, we can derive (using . for an empty context):<br /><br /> A valid ; . |- []A true<br /><br />But not:<br /><br /> . ; A true |- []A true<br /><br />The []I rule is essentially similar to the "extend" function, but expressing it using two kinds of assumptions leads to the system having particularly nice properties. Dually, there's a second kind of conclusion for possibility, related to the diamond <> modality.<br /><br />It should be clear that [] corresponds to a comonad, and <> corresponds to a monad. Further the two are related in a very particular way, as required by modal logic. As a result, e.g., <> is strong with respect to the first context but not the second.<br />Rowan Davieshttp://www.blogger.com/profile/02888491281001274822noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-52982133616385345372013-02-19T16:35:34.983-08:002013-02-19T16:35:34.983-08:00This post is about comonads more than it is about ...This post is about comonads more than it is about this object oriented programming. This post introduces comonads as a subset of object oriented programming, specifically the fluent programming style pioneered by JQuery. However, I am not done with the analogy and I already know of several other striking parallels to OOP that I have not written up yet, including parallels to inheritance and traits.<br /><br />It does not bother me in the least, though, that comonads do not cover the full spectrum of OOP as OOP had become an umbrella term for a wide variety of unrelated functionality. I'm simply showing that comonads cover a surprising subset of OOP functionality without any built-in language support for OOP.<br /><br />One thing I find endearing about Haskell is that, unlike other languages it does not compromise its elegance or simplicity in order to be a "multi paradigm language". Rather it takes the principled position that functional programming is sufficient to implement all other forms of programming. This post and future posts build on that idea to show how even OOP can be a subset of functional programming.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-14633467126314045842013-02-19T16:23:09.097-08:002013-02-19T16:23:09.097-08:00Actually, that was a typo (or perhaps a Freudian s...Actually, that was a typo (or perhaps a Freudian slip!). I will fix it soon.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-48381679341666062932013-02-17T20:08:35.559-08:002013-02-17T20:08:35.559-08:00Hi Gabriel,
Cool posting!
Is there a typo when you...Hi Gabriel,<br />Cool posting!<br />Is there a typo when you first introduce the method desugaring?<br />It looks like there may be too many wb's (or _wb's) and not enough<br />wc's (or _wc's)...myzoskihttp://www.blogger.com/profile/02622704681931775367noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-52335709752654564762013-02-17T11:31:56.127-08:002013-02-17T11:31:56.127-08:00And here I was starting to think that designing pr...And here I was starting to think that designing programs through the communication of possibly stateful, ideally referentially-transparent entities over well defined interfaces (pure pipes/lazy pure fp/pure TPL Dataflow Block/) was object-orientation done right! That is, if OOD is to be defined by its published benefits.ShowPonyhttp://www.blogger.com/profile/07870841144965376439noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-55209966307998995982013-02-17T06:33:54.216-08:002013-02-17T06:33:54.216-08:00Hi Gabriel,
you often write "objected-oriente...Hi Gabriel,<br />you often write "objected-oriented" and "objected oriented" which may be a subtle pun underlining your thesis that Haskell frowns upon object-orientation. Is this intentional, or did you intend to use the common term "object-oriented"?heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-30193737810632160922013-02-16T04:12:33.233-08:002013-02-16T04:12:33.233-08:00Thanks for all the links. I'm just a graduate...Thanks for all the links. I'm just a graduate student doing bioinformatics with a keen interest in Haskell but the more I use the language the more I get sucked up into computer science.<br /><br />Regarding the Kieburtz paper, many of the OI functions he proposes have that type, such as:<br /><br />stdPutChar :: OI Char -> ()<br /><br />That type signature sort of bothers me, because I would expect there to be only one function (up to isomorphism) with that type, namely:<br /><br />stdPutChar _ = ()<br /><br />... but maybe that's a faulty intuition that I've built from using Haskell. Or maybe he had the right idea, but it belongs in a different category other than the category of Haskell functions, i.e.:<br /><br />stdPutChar :: C (OI Char) ()Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-59653436813280505262013-02-15T11:53:23.348-08:002013-02-15T11:53:23.348-08:00I'm doing with with Amr Sabry at Indiana Unive...I'm doing with with Amr Sabry at Indiana University, specifically on extending stuff done in his student Roshan James' thesis on "information effects". They have a paper from POPL '12 that's pretty rad: http://delivery.acm.org/10.1145/2110000/2103667/p73-james.pdf?ip=129.79.245.33&acc=ACTIVE%20SERVICE&CFID=225224900&CFTOKEN=62904902&__acm__=1360956345_7a3d0778ff13776dc280f100adbe9ad9 , if it's not paywalled for you.<br /><br />As far as the base functor is concerned, I'm not actually sure---I'm not up on my categorical logic, unfortunately. Some of Steve Awodey's lecture notes talk about <> and [] as a monad and a comonad; if you ctrl+f "modal" in http://www.andrew.cmu.edu/course/80-413-713/notes/chap10.pdf it's the page with the 2nd and 3rd result. I'm not sure if that's helpful or not, though. Maybe that means they're not free after all? I'm not sure. I think I'd heard someone say they were, but maybe I'm misremembering; I do know that the only operations available on <> (and lax) are only return and bind, though.<br /><br />Box isn't a monad: the intro rule only allows you to use persistent assumptions when trying to prove []A, erasing your regular context. So if you tried to prove A -> []A, you'd stick A in your context, then immediately forget it. It's bad news! But this means you can prove A -> []A for exactly those A which are equivalent to T. There's no corresponding rule for <> or () that allows you to get out of the monad exactly when the thing in the monad is bottom, though.<br /><br />And yeah, I guess I might be conflating freeness with the idea that only a certain set of operations is allowed, *and no more*. I guess "cofree" doesn't make sense in that interpretation, though, or at least no sense I can make of it. But the idea is that if you can *only* use those operations, then there's no way to get out of the fancy monad, and no way to get into the fancy comonad. This property is definitely desirable for the IO monad, and Kieburtz seems to have assumed it for his OI comonad.<br /><br />I should also note that there are tons of different modal logics; I believe the one I'm referring to is canonically called S5 (or IS5, I guess, since intuitionistic logic is where it's at). The paper I linked to is a good reference, if you have the time for it; Frank Pfenning also has some awesome lecture notes on his site. I'd probably recommend them if you want to start learning more about logic in general. He's got an undergrad constructive logic course (http://www.cs.cmu.edu/~fp/courses/15317-f09/) that might be helpful for some basics, but they're also covered briefly in the beginning of his modal logic (http://www.cs.cmu.edu/~fp/courses/15816-s10/) and linear logic (http://www.cs.cmu.edu/~fp/courses/15816-s12/) course notes. Also, I dunno if you're an undergrad or a grad student or a postdoc or professor or industry person or hobbyist or what, but have you heard of OPLSS (http://www.cs.uoregon.edu/Activities/summerschool/summer13/)? Frank gave a great series of talks on logic last year, and iirc he does it pretty much every year.<br /><br />With respect to the Kieburtz paper, why do you bring up a -> () ? Maybe there's an obvious reason to do so, but I'm missing it, if so. Also, you mention that it'd be weird for an abstraction and its dual to have the same use, which is intuition I share, but it can be wrong. In particular, the reader monad is isomorphic to the product comonad (as proved in http://www.cs.ioc.ee/~tarmo/papers/cmcs08.pdf, which is a great read if you haven't seen it already). So there can be some overlap going on. I also do like the idea of passing around a "token" of sorts that gives you permission to access IO stuff, but you'd need at the very least a linear type system to be able to keep track of it, and using it as a modality is kind of trivial, so yeah, maybe not the best approach.Zach Sparkshttp://www.blogger.com/profile/04255124858521461420noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-29489617173755281002013-02-15T07:19:10.532-08:002013-02-15T07:19:10.532-08:00You're right. I added the fixity definition.You're right. I added the fixity definition.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-86430575815434909832013-02-15T07:18:45.050-08:002013-02-15T07:18:45.050-08:00Thanks! I fixed them.Thanks! I fixed them.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-31768604385860579262013-02-15T07:16:31.292-08:002013-02-15T07:16:31.292-08:00I just glossed over it. This actually has some fa...I just glossed over it. This actually has some fascinating material for additional uses of comonads. I particularly liked the liveness analysis application. I will have to take time to digest it some more.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-77078839308321268822013-02-15T07:09:03.934-08:002013-02-15T07:09:03.934-08:00Could you elaborate more on your research about pr...Could you elaborate more on your research about preserving information? This is a topic that has fascinated me as well.<br /><br />My intuition about CoIO is that if you were to implement it in terms of CoFree, the key function the user would write would have type:<br /><br /> forall r . CoFree f r -> r<br /><br />In other words, the way you define 'CoIO' behavior is simply by selecting one 'r' value from the CoFree stream. The universal quantification keeps you honest and forces you to select a value from the CoFree comonad.<br /><br />For example, the 'r' values could just be assembly code, and depending on which 'r' you select decides which program you compile. However, that approach does not work well for various reasons, but I'm just throwing that crazy idea out there.<br /><br />I've never read the "Comonads and Codata" paper before, but I remember that I rejected a similar line of thinking because any function of type "a -> ()" should be isomorphic to "()", which means that there should only be one such function. I'm not sure that comonads are supposed to be able to encapsulate effects, particularly when monads do so incredibly well. It would seem odd to me for both an abstraction and its dual to both overlap in functionality.<br /><br />I'm going to preface the logic stuff by saying that logic is totally a weak point of mine. I'm not familiar with the concrete rules of most logic systems since almost everything I've learned about computer science is just a side effect of programming in Haskell, but I'll make an effort to try to follow what you are saying by consulting the relevant Wikipedia articles. :)<br /><br />So if diamond is possibility, and it's a monad, then we'd expect that:<br /><br /><><> p -> <> p<br /><br />p -> <> p<br /><br />So far so good. If it's a free monad, then there must be an adjunction (I'm going to bastardize notation by mixing logic and Haskell):<br /><br />(f? p -> m p) ~ ((Monad m) => <> p -> m p)<br /><br />See, here's the part that's a bit confusing. A free monad requires defining some sort of base functor, but in the case of '<>' it's not clear what that base functor is. Or in other words:<br /><br /> Free f p = <> p implies f = ?<br /><br />A free monad is at heart a list of 0 or more nested applications of the given functor, so I'm wondering what modal logic functor, when applied 0 or more times, is equivalent to the possibility operator.<br /><br />The other part that's curious is that it seems like box also should be a monad:<br /><br />p -> [] p<br /><br />[][] p -> [] p<br /><br />Are those valid rules in modal logic?<br /><br />Also, there's nothing about comonads that says you can't build them. A key point to remember is that the definitions of monads and comonads are positive: they specify a uniform interface to what you can do, and don't forbid anything. Specifically, they don't forbid you from being able to unwrap the monad (with the Identity, Reader, and State monads being the canonical counter-examples). However, these unwrapping operations are non-uniform across monads, whereas the monad operations are uniform across them, so it's better to think of the monad class as simply specifying the uniform property that all monads share.<br /><br />So in the same way that I don't necessarily expect a monad to be unwrappable, I also don't expect a comonad (even the CoIO comonad) to be uncreatable.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-90704426027562394802013-02-15T05:08:15.908-08:002013-02-15T05:08:15.908-08:00Hey, your 'exampleHistory' snippet won'...Hey, your 'exampleHistory' snippet won't compile, because :< has default fixity. Making it infixr 5 (like cons) fixes the issue.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-40984486798998012092013-02-15T01:47:06.439-08:002013-02-15T01:47:06.439-08:00Wow, nice! There's a small typo in discussion ...Wow, nice! There's a small typo in discussion of the Iterator pattern: "to be remain consistent" -> "to be consistent" or "to remain consistent". Also, I think you meant <br /><br />let builder1 = defaultConfig # profile'<br /><br />instead of <br /><br />>>> let builder1 = defaultBuilder # profile'Jan Stolarekhttp://ics.p.lodz.pl/~stolarek/blognoreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-60388260905470353142013-02-14T22:07:14.806-08:002013-02-14T22:07:14.806-08:00have you seen tomas petricek's "Coeffects...have you seen tomas petricek's "Coeffects: The Essence of Context Dependence"? just a draft but looks interesting (and relevant.)<br /><br />http://www.cl.cam.ac.uk/~tp322/drafts/coeffects.htmlBenhttp://archerlabs.netnoreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-76310237042036870952013-02-14T20:18:30.152-08:002013-02-14T20:18:30.152-08:00Hm, cool. I'll have to think about the Kleisli...Hm, cool. I'll have to think about the Kleisli category stuff more; I'm not as up on category theory as I'd like to be. I'd be interested to see more about case analysis with the cofree comonad; I'm not entirely sure what that means, exactly.<br /><br />In the Reddit thread, you mention CoIO; I assume you've read Kieburtz's "Codata and Comonads in Haskell"? He describes the OI comonad there, and some possible ways of using it, but apparently it has issues (http://www.haskell.org/pipermail/haskell-cafe/2006-November/019265.html). I think it's possible to use it for effects in a more restricted setting where information is preserved (coincidentally, my research is on information preservation...), but in a more traditional setting, your intuition matches mine: it seems like OI a (or CcOI a) "should" be the type of pure values of type a. If that's the case, it's possible that it would be more productive (ha) to explore it in an eager language (Idris, perhaps). I think I read something to this effect elsewhere, but I can't remember where.<br /><br />One side note that I think is interesting: correct me if I'm wrong, but I believe that in modal logic, the diamond/"possibility" operator can be thought of as the free monad, and the lax operator can be thought of as the free strong monad. The box/"necessity" operator, however, doesn't act like the free [costrong?] comonad, because you have the intro rule:<br /><br />\Delta, \empty |- A<br />---------------------[]I<br />\Delta, \Gamma |- []A<br /><br />This is going off of the presentation in Pfenning-Davies (http://www.cs.cmu.edu/~fp/papers/mscs00.pdf), in particular.<br /><br />But anyway, this rule gives you things like T |- []T which seems...wrong, given that there's no corresponding theorem <>_|_ |- _|_ (pardon the ascii). Again, my category theory is rusty, so maybe that's acceptable, but it seems kind of off; my intuition says you shouldn't be able to get into the cofree comonad (or whatever) unless you're already in it!<br /><br />Anyway, that's probably a bit rambly at the end there, sorry. Maybe it'll be useful? *shrug* Zach Sparkshttp://www.blogger.com/profile/04255124858521461420noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-37905873423527815222013-02-14T15:46:44.935-08:002013-02-14T15:46:44.935-08:00Wow, that first link is really good. It very clos...Wow, that first link is really good. It very closes mirrors some observations and intuitions I built in the process of working with comonads. For example, comonads and `method` notation resist embedding any effects in between steps. I just answered another person on reddit who asked me about embedding these comonadic computations within a Kleisli category:<br /><br />http://www.reddit.com/r/haskell/comments/18isiu/comonads_are_objects/c8f9fw0<br /><br />The summary is that comonads stubbornly resist any useful interleaving of monadic side effects, which exactly mirrors how that link envisioned the use of these negative recursive types as views.<br /><br />Moreover, the idea of using comonads as a more powerful case analysis is strongly suggested by "THE" comonad: the cofree comonad. If you combine the cofree comonad with method syntax, you get a DSL for case analysis on the base functor of the cofree comonad.<br /><br />I am familiar with Dominic Orchard's codo notation, and the entire reason I investigated this line of reasoning was that I was unsatisfied with his approach, which didn't behave the way I expected the rightful dual to 'do' notation to behave. For example, he was still binding unwrapped values within the monad, which seemed intuitively incorrect, and the application of maintaining simultaneity only made sense for a couple of comonads and not all of them.<br /><br />However, the thing that was most unsatisfying about his approach was the fact that the desugaring was so complicated and required additional structure (i.e. ComonadZip) on top of the Comonad class to implement correctly.Gabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-52742453025954514342013-02-14T14:10:12.548-08:002013-02-14T14:10:12.548-08:00This is pretty fascinating! I've toyed around ...This is pretty fascinating! I've toyed around with comonads a bit, but it never occurred to me to think of them as objects.<br /><br />I've also seen objects presented as negative recursive types (cf http://requestforlogic.blogspot.com/2012/03/what-does-focusing-tell-us-about.html); I'm wondering if there's some way of looking at them that unifies both perspectives? I'm guessing they're orthogonal, though, thanks to the many meanings of the word "object"; Cook-objects appear to be primarily concerned with negativity & mutual recursion, whereas comonadic objects (correct me if I'm wrong) appear to primarily concerned with the inner state of an object. It's interesting (though perhaps only superficially) that both approaches are dual to familiar approaches (datatypes and monads, respectively).<br /><br />Are you familiar with Dominic Orchard's codo-notation (http://www.cl.cam.ac.uk/~dao29/drafts/codo-notation-orchard-ifl12.pdf)? It appears to be very similar to your method notation, but without the implicit "this" argument. There's also od-notation, but a few moments of quick googling didn't reveal a link to it (though they did reveal an eye doctor in New Hampshire! http://www.eyesightnh.com/new-hampshire/susan-haskell-o-d-f-a-a-o..htm).zacharyzsparkshttp://www.blogger.com/profile/04255124858521461420noreply@blogger.com