tag:blogger.com,1999:blog-11295132.post4013221249502217550..comments2017-04-17T12:25:44.891-07:00Comments on A Neighborhood of Infinity: The Mother of all MonadsDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger29125tag:blogger.com,1999:blog-11295132.post-11261716136257617632017-01-07T19:21:58.454-08:002017-01-07T19:21:58.454-08:00Why does everyone feel the need to make the catego...Why does everyone feel the need to make the categorical semantics here way more complex then it needs to be?<br /><br />If you read further into Andrzej Filinski's work, you'd come across the paper "Declaritive Continuations: an Investigation of Duality in Programming Language Semantics". In it, Filinski describes a symmetric lambda calculus wherein continuations are given a dual semantics. <br /><br />The symmetric lambda calculus is the internal language to a bi-cartesian bi-closed category, which is a category which has a terminal object (1), products (⊗), exponential map (⇒), initial object (0), coproduct/sums (⊕), and crucially, co-expontials (⇐), also sometimes called subtraction. <br /><br />Under this identification, defining do-notation is now quite simple, it's the co-evaluation map:<br />do:[y←x] := ((y ⇐ x)⊕x)Keith Petersonhttp://www.blogger.com/profile/05978285067695033674noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-3767929588729595512016-08-19T06:11:53.522-07:002016-08-19T06:11:53.522-07:00Dan, Isn't this post more clearly explained by...Dan, Isn't this post more clearly explained by the construction in Section 3.3 of Wadler (1992), which shows how to embed any arbitrary monad into the continuation monad?<br /><br />Philip Wadler, The Essence of Functional Programming, POPL 1992.Philip Wadlerhttp://www.blogger.com/profile/12009347515095774366noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-70052683948783028352015-09-10T19:21:02.191-07:002015-09-10T19:21:02.191-07:00Trying to wrap my head around this... with ex7, wo...Trying to wrap my head around this... with ex7, would you be able to get a way with<br /><br />> ex7 = do<br />> a <- return 1<br />> b <- Cont (\fred -> fred 10 `mplus` fred 20)<br />> return $ a+b<br /><br />to make it agnostic to any implementation MonadPlus?Dhttp://www.blogger.com/profile/12899102576877916413noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-11301683498708603612014-03-14T15:07:52.604-07:002014-03-14T15:07:52.604-07:00The State arrow factors into a monad.
(a,s) ->...The State arrow factors into a monad.<br /><br />(a,s) -> (b,s) is isomorphic to a -> s -> (b, s) whi<br />ich is a -> State s b<br /><br />That s why you can define it for State, but not every arrow factors that way.Edward Kmetthttp://www.blogger.com/profile/16144424873202502715noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-38663694165298513542014-03-14T15:07:04.967-07:002014-03-14T15:07:04.967-07:00The State arrow factors into a monad.
(a,s) ->...The State arrow factors into a monad.<br /><br />(a,s) -> (b,s) is isomorphic to a -> s -> (b, s) whi<br />ich is a -> State s b<br /><br />That s why you can define it for State, but not every arrow factors that way.Edward Kmetthttp://www.blogger.com/profile/16144424873202502715noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-46323386127352323712014-03-14T14:08:20.509-07:002014-03-14T14:08:20.509-07:00I see, the syntax reuse is a nice effect. In regar...I see, the syntax reuse is a nice effect. In regard to "i", I tried defining a comparable function for arrows to reuse arrow syntax, but it seems impossible (no way to pass the result of x to the continuation). This is strange because e.g. put/get are simple to define for the Cont Arrow simulating the State Arrow, which then can use arrow syntax just fine. Syntax reuse is thus not limited to monads, but the "i" function might be? (I'm not a theory expert.)Sean Kanaleyhttp://www.blogger.com/profile/06567427255740163613noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-30077761930180278942014-03-14T11:32:33.944-07:002014-03-14T11:32:33.944-07:00> one could claim that continuations are the mo...> one could claim that continuations are the mother of all everythings<br /><br />Sure. Every computation can be seen as some stuff being provided to a continuation which then runs with it. But I'm talking specifically about monads. Among the collection of monads the continuation monad provides a universal monad in which all others can be embedded. The function 'i' is in fact a monad morphism so this gives a principled way to use continuations to perform the function of any monad rather than simply saying "I can do anything because at the end of the day code is all just a bunch of machine code".<br /><br />This isn't just a vacuous statement. As I mentioned, given any language with a syntax for continuations you have the possibility of reusing that notation for monads. For example Python has linear continuations (via generators) so you can use this as a syntax for any of the 'linear' monads (like Identity, Maybe and Writer I think).Dan Piponihttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-18289668734809397702014-03-14T10:44:06.726-07:002014-03-14T10:44:06.726-07:00I believe what you are getting at is that Identity...I believe what you are getting at is that Identity has no input by which to parameterize its behavior. It can only ever give effectively pure code, and IdentityT can only give back the contained monad, but Cont actually lifts pure code into a monad through the hook provided by the continuation function. My analogy with id would have been better if I said id converts assembler into a Haskell function, e.g. id (mov bx,3; add ax,bx; etc.) where id is the context that builds a function (but otherwise does not affect the provided behavior), assigns the input parameter to ax, etc. Cont and id would then both set up a surrounding context by which more primitive operations define the container type.<br /><br />I would think this idea of containing lower stuff with nearly-id-higher stuff (contified stuff) would hold in general, and one could claim that continuations are the mother of all everythings. Or is there some type class where this transformation fails?Sean Kanaleyhttp://www.blogger.com/profile/06567427255740163613noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-75128987320112986022014-03-12T18:46:44.782-07:002014-03-12T18:46:44.782-07:00@Sean,
Suppose that Haskell do-notation only supp...@Sean,<br /><br />Suppose that Haskell do-notation only supported the Identity type, not the full Monad type class. How would you leverage it to get something as close as possible to the original do-notation that works with any Monad.Dan Piponihttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-5854213653445641082014-03-12T10:08:24.127-07:002014-03-12T10:08:24.127-07:00At first it seems amazing that Cont can do anythin...At first it seems amazing that Cont can do anything, but an almost analogous statement shows it's a ruse:<br /><br />"The identity function is the mother of all functions." -- one can simulate (+3) with id (+3).<br /><br />That statement is actually closer to saying IdentityT is the mother of all monads, e.g. IdentityT (State Int) = State Int. But ContT is just CPS-ified IdentityT. The Cont monad doesn't *do* anything except for what it's told to do, similar to id.<br /><br />For example, when you simulated the list monad you did so by hard-coding in the implementation of list's bind then wrapping it in Cont, just like (+3) can be wrapped in id. All Cont does is defer computation, so the actual computation that is deferred is what truly defines it. In this sense the statement that Cont can do anything suddenly seems vacuous! It can do anything because it does nothing except for the parameter/inlined code telling it exactly what to do! We can also say an empty .hs file is the mother of all Haskell programs.Sean Kanaleyhttp://www.blogger.com/profile/06567427255740163613noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-36623522470034639012012-05-18T06:14:53.320-07:002012-05-18T06:14:53.320-07:00I was trying to figure this out again. Here is th...I was trying to figure this out again. Here is the code as it stood in 2008 running on Hugs: http://codepad.org/iJyF916i Here are literate and delit-ed versions presupposing the new `type Cont a = ContT a Identity` as sigfpe suggestedmichaeltnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-17826868801375804212011-12-03T10:41:48.246-08:002011-12-03T10:41:48.246-08:00Tyr,
Try replacing occurrences of the constructor...Tyr,<br /><br />Try replacing occurrences of the constructor "Cont" with the function "cont". After this I can load the .lhs file in ghci and it all works. (I'm using version 2011.2.0.1 of the Haskell Platform.) <br /><br />(This was posted by 'anonymous' but I accidentally deleted it so this is a repost by me.)sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-44256291997537734512011-11-22T08:46:08.950-08:002011-11-22T08:46:08.950-08:00The code is broken now. :(The code is broken now. :(Tyrhttp://www.blogger.com/profile/17404408031973346085noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-85870733947363908182009-12-03T17:54:57.769-08:002009-12-03T17:54:57.769-08:00Secret Agent for the Dumb,
>>= basically ap...Secret Agent for the Dumb,<br /><br />>>= basically applies a function to each element of a list, and then flattens the entire result. But I think you got that already.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-22874499627018860992009-04-19T18:15:00.000-07:002009-04-19T18:15:00.000-07:00you lost me a bit at "ex8". I think what...you lost me a bit at "ex8". I think what I see is that [10,20] >>= fred is a bind in the LIST monad, and not in the continuation monad, as is the final "return" in "runCont ex8 return." I think "fred" has type "x->[x]" so [10,20]>>=fred means 'bind [10,20] to x, build [[10,20]] and flatten one level, producing [10,20]", which, if memory serves, is what the >>= of the list monad does. Have I got it?Secret Agent for the Dumbhttp://www.blogger.com/profile/00115031720080635093noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-34994662462122596922009-01-05T10:08:00.000-08:002009-01-05T10:08:00.000-08:00sigfpe/rory:As a sketch for how 'ContT is terminal...sigfpe/rory:<BR/><BR/>As a sketch for how 'ContT is terminal':<BR/><BR/>If you discard the information about the return value's type through quantification (using a forall, or less safely just using the current continuation in a 'very limited' manner) then you can view ContT as a right Kan extension of a functor F along itself. That can be viewed as a limit taken pointwise over a comma category - just invert the colimit example in the wikipedia article on Kan extensions to take a limit of Ran instead a colimit of Lan. That limit is a terminal object in a category of cones. <BR/><BR/>ContT is slightly larger than this, in that you CAN abuse the current continuation. That said, to define a codensity monad and lift/lower monadic actions into it as you have done, you do not use that extra functionality.<BR/><BR/>The fact that you can lift any monad into it (by CPS transformation) is just a consequence of the existence of the codensity monad, ContT is actually a bit bigger than it needs to be.<BR/><BR/>This is all just another way to say that a CPS transformation can always be applied. <BR/><BR/>And you can take away from this, somewhat tongue in cheek, that continuations are slightly more complicated than they need to be to do the job. ;)Edward Kmetthttp://www.blogger.com/profile/16144424873202502715noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-54133402714657366562009-01-02T18:02:00.000-08:002009-01-02T18:02:00.000-08:00Roly,> What does all this mean categorically?I ...Roly,<BR/><BR/>> What does all this mean categorically?<BR/><BR/>I had the same thought as you - Cont must be terminal or final in some category. But I haven't figured out what category that is.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1828424934575797292008-12-30T05:17:00.000-08:002008-12-30T05:17:00.000-08:00Great post!>Many languages with support for con...Great post!<BR/><BR/>>Many languages with support for continuations should be extensible to support monads<BR/>I'd phrase it a little differently: language with support of continuations automatically supports monads with natural syntax.<BR/>Perhaps it is worth to mention that one needs delimited control operators to simulate monadic do-notation (in case of Control.Monad.Cont the 'runCont' function is a control delimiter).Glebhttp://www.blogger.com/profile/12646910389871722935noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-32791795328693194612008-12-28T11:45:00.000-08:002008-12-28T11:45:00.000-08:00If you look in category-extras there is actually a...If you look in category-extras there is actually a monad that boxes up this functionality and reflects this idea; the "codensity monad," aka the monad generated by a functor basically represents a CPS transform.<BR/><BR/>http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/src/Control-Monad-Codensity.html<BR/><BR/>Your run corresponds to my lowerCodensity and i corresponds to liftCodensity.<BR/><BR/>The rest just relies on the fact that:<BR/><BR/>newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b }<BR/><BR/>which can also be read as forall r. ContT (m r) a is a monad regardless of m, (it doesn't even have to be a functor!)<BR/><BR/>This monad has nice performance characteristics, because it just reflects a CPS transform of the code.<BR/><BR/>A variation on the presentation is available here:<BR/><BR/>http://www.haskell.org/haskellwiki/Performance/Monads<BR/><BR/>Since this represents a CPS transform of the code and is a monad in its own right if the bind operation of the monad is expensive, as in say most free monads, you can change the asymptotic behavior of code that is running in the monad.<BR/><BR/>Janis Voigtlaender has a paper on the topic, in which you'll recognize the type 'C' that he uses as the Codensity monad above.<BR/><BR/>http://wwwtcs.inf.tu-dresden.de/~voigt/mpc08.pdf<BR/><BR/>Moreover, if you are looking for a window to understanding Kan extensions, you can view the codensity monad as the right Kan extension of a functor along itself.Edward Kmetthttp://www.blogger.com/profile/16144424873202502715noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-68217823316199910662008-12-25T02:11:00.000-08:002008-12-25T02:11:00.000-08:00What does all this mean categorically? I haven't ...What does all this mean categorically? I haven't yet tried to understand what monad morphisms are (other than that they must be natural transformations that preserve the extra structure of a monad), but does the continuation monad turn out to be initial or terminal in a suitable category?Roly Pererahttp://www.blogger.com/profile/10168144731270158487noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-68847485219355611272008-12-25T01:22:00.000-08:002008-12-25T01:22:00.000-08:00I wrote a monads module in scheme few years ago. ...I wrote a monads module in scheme few years ago. I wanted to use it for all monads, but Scheme had no namespace or type class. Therefore, the only way is extract the core part of monads (the mother of all monads). This is the major code:<BR/><BR/>(define bind<BR/> (lambda (a b)<BR/> (lambda (k)<BR/> (a (lambda v ((apply b v) k))))))<BR/><BR/>(define return<BR/> (lambda v<BR/> (lambda (k)<BR/> (apply k v))))<BR/><BR/>(define run-IO<BR/> (lambda (m)<BR/> (m values)))<BR/><BR/>(define run-State<BR/> (lambda (m . s)<BR/> (apply (m (lambda r (lambda _ (apply values r)))) s)))<BR/><BR/>(define State-set<BR/> (lambda v<BR/> (lambda (k)<BR/> (lambda s<BR/> (apply (apply k s) v)))))<BR/><BR/>(define return-List<BR/> (lambda l<BR/> (lambda (k)<BR/> (apply append (map k l)))))<BR/><BR/>(define run-List<BR/> (lambda (m)<BR/> (m list)))<BR/><BR/>I didn't know it is correct or not. After I read you post, I understand I've acturally written a Cont monad and work out other monads with it, same as what you did. You solved my long time question!Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-77898579710992943552008-12-24T19:17:00.000-08:002008-12-24T19:17:00.000-08:00AliPang: If you're on Gentoo (or perhaps some othe...AliPang: If you're on Gentoo (or perhaps some other *nix with a conservative package manager), you may have to install dev-haskell/mtl (or your *nix's equivalent package name), since GHC does not pull it in as a dependency. Be forewarned, if you are indeed using Gentoo, it may take awhile to compile.Cthulhonhttp://www.blogger.com/profile/12656647628788096090noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-26736868839285715292008-12-24T17:50:00.000-08:002008-12-24T17:50:00.000-08:00AliPang,Try copying this entire post into a file c...AliPang,<BR/><BR/>Try copying this entire post into a file called test.lhs and running that in ghci. If that doesn't work, I wonder if you're missing some libraries. (I only know about ghc.)sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-6423661707420777652008-12-24T17:36:00.000-08:002008-12-24T17:36:00.000-08:00I wanted to learn more about continuations for a w...I wanted to learn more about continuations for a while. But how do you get Haskell to recognize Control.Monad.Cont? I get a "Could not find module" error when I try to use it. <BR/><BR/>(And, no, I couldn't find anything useful through Google, though I will happily accept a "Let me google that for you" link :P)AliPangnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-81194379498646404712008-12-24T17:18:00.000-08:002008-12-24T17:18:00.000-08:00Ah, I missed the total cleverness of i. Thanks!Ah, I missed the total cleverness of i. Thanks!augustsshttp://www.blogger.com/profile/07327620522294658036noreply@blogger.com