tag:blogger.com,1999:blog-11295132.post5498567246174830347..comments2019-02-21T03:59:37.273-08:00Comments on A Neighborhood of Infinity: Using Lawvere theories to combine effectsDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger8125tag:blogger.com,1999:blog-11295132.post-12181603416831183152013-02-26T12:00:03.092-08:002013-02-26T12:00:03.092-08:00@Gabriel Is there any guarantee of uniqueness, tho...@Gabriel Is there any guarantee of uniqueness, though?Joseph Abrahamsonhttp://jspha.comnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-27765673417057574092012-04-28T20:23:51.519-07:002012-04-28T20:23:51.519-07:00I thought that you could verify monad transformers...I thought that you could verify monad transformers were implemented correctly by checking the monad transformer laws, which are just the functor laws from the lower monad's Kleisli category to the higher monad's Kleisli category.Gabriel Gonzalezhttps://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-65206521282288848272012-02-14T07:37:23.709-08:002012-02-14T07:37:23.709-08:00@migmit,
Maybe I haven't made something clear...@migmit,<br /><br />Maybe I haven't made something clear. I don't care about those FreeX types. They're just intermediate steps in the construction. The thing I want is the quotient. The FreeX types are just ways to construct the sets of arrows we need. But those types are useless for implementing effects without the quotient. I most certainly do admit defeat in the sense that I can't write code to automatically construct the appropriate quotient. But I can do it manually and that's what I illustrated.<br /><br />I'm not using Lawvere theories to justify anything. I constructed the types for the combined effect by reading a paper on Lawvere theories and finding the closest approximating Haskell code. I then noticed that the construction, for this case, gave the same result as using monad transformers for the two effects. That doesn't necessarily happen every time.<br /><br />I like this approach because the resulting type was determined uniquely given the two starting effects. Forming the monad transformer requires guesswork and in some sense, even if you make a guess that works for you, there's no definition against which you can check whether the thing you've constructed is in any sense the "right" one. (You can apply the transformer to the identity monad and see if you get back the original monad, but there can be multiple constructions with this property with no principled way of distinguishing between them.)<br /><br />You can combine any two type classes described by algebraic laws this way. In some sense it's universal, but not all type classes are described by algebraic laws. That's not a trivial observation.<br /><br />And I'll say again: the code for the FreeX classes is entirely useless. I was simply implementing in Haskell the halfway point in the mathematical construction. I could have left the halfway point entirely as mathematics and left out the FreeX type. But I think Haskell notation is better than the construction used in the mathematics papers. (Eg. compare Andrej's description of the arrows in terms of strings of symbols: http://mathoverflow.net/questions/70162/why-lawvere-theories-have-finite-products-and-more/70182#70182)sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-35537701599325683592012-02-13T22:42:08.671-08:002012-02-13T22:42:08.671-08:00It's a very, VERY big modulo. So, as I see it,...It's a very, VERY big modulo. So, as I see it, that's what happened:<br /><br />1) You've created some "combined monad" (I'll get to that part in a moment).<br /><br />2) You showed that for any monad that satisfies some properties, there is a very natural map from your combined monad to that one.<br /><br />3) You've discovered that a WriterT [] monad satisfies said properties.<br /><br />4) So, you have a map from your combined monad to WriterT []. So far so good.<br /><br />5) Based on that, you claim that your monad and WriterT [] are essentially the same. Sorry, but I don't buy it. There is just a map from one thing to another, it doesn't make them even remotely similar.<br /><br />> the goal is to combine effects, not monads.<br /><br />Well, you've explicitly said that you combined monads.<br /><br />As for the construction of this "combined monad"... It's just a way to turn everything to anything. Whenever you have some type Foo, and you think "oh, how lovely it would be if it was an instance of class Bar", well, your last resort is to use continuations, defining newtype FooBar = FooBar (forall a. Bar a => (Foo -> a) -> a). Sure, it's a neat trick... but also a kind of admitting defeat, since it's so universal. It's kind of saying "I can't do it properly, but I'll do it anyway". Not that I've never done it myself - of course I did. But it's not justified by mentioning some clever theory (Lawvere theories this time) and then throwing away almost all of it (laws, this time). It feels like... cheating.migmithttps://www.blogger.com/profile/06981055611018991476noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-75503771342424665952012-02-13T07:00:06.748-08:002012-02-13T07:00:06.748-08:00@migmit,
I'm a bit confused when you say Free...@migmit,<br /><br />I'm a bit confused when you say FreeMMonoid is nothing similar to WriterT w [] when I show that one is essentially the other modulo equivalance with algebra laws. And as the title says, the goal is to combine effects, not monads. It just so happens that for this example there is some overlap with monads. And if you can combine other things this way, that's all well and good. And I've no intention of hiding the connections with continuations. And I'm not sure why Lawvere theories are overkill when the construction of the arrows from a Lawvere theory is, modulo equivalence, a line of Haskell. (What I did omit was the motivation for the definition of compatibility which is a small category diagram.)sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-77105066097156348192012-02-12T23:35:15.464-08:002012-02-12T23:35:15.464-08:00> We combined the list monad and the writer mon...> We combined the list monad and the writer monad to get a new monad. We did it without using monad transformers<br /><br />We did? I haven't noticed. At least, I can't see an "instance Monad" anywhere.<br /><br />Oh, maybe you mean that FreeMMonoid is also a monad? That's obviously true, but your claim that "the result was the same as using a monad transformer" is far from being true. FreeMMonoid is just a special case of a continuation monad (yes, I know, you've tried to hide this "a -> b" extra argument, but you didn't hide it well enough). It's a pretty useful trick, but it's NOT similar to anything like "WriterT w []". And this trick is not for monads only; you can combine pretty much everything in this way.<br /><br />Also, Lawvere theories? That seems to be a HUGE overkill for that simple trick.migmithttps://www.blogger.com/profile/06981055611018991476noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-18017972168996657822012-02-12T10:50:13.392-08:002012-02-12T10:50:13.392-08:00When you say "Leaf x1 `mappend` (Leaf x2 `map...When you say "Leaf x1 `mappend` (Leaf x2 `mappend` (... mempty))" do you mean (lowercase) "leaf"?Tomhttp://web.jaguarpaw.co.uk/~contact/noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-63906041344436488082012-02-11T20:14:46.881-08:002012-02-11T20:14:46.881-08:00I enjoyed reading these posts as well as reading a...I enjoyed reading these posts as well as reading all those old ones again. :)<br /><br />Am I correct in understanding that having the compatibility conditions (as opposed to none) is in practice always what you want when combining monadic effects? Are there any examples where you'd naturally not want them, or where you'd want ad hoc compatibility conditions?Anonymousnoreply@blogger.com